1<?xml version="1.0" encoding="utf-8"?> 2<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN" 3"http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd"> 4<html xmlns="http://www.w3.org/1999/xhtml" lang="en" xml:lang="en"> 5<head> 6<!-- 2024-10-20 Sun 23:33 --> 7<meta http-equiv="Content-Type" content="text/html;charset=utf-8" /> 8<meta name="viewport" content="width=device-width, initial-scale=1" /> 9<title>Decidability in the One-Point Compactification of â</title> 10<meta name="author" content="[[https://armkeh.github.io][Mark Armstrong]] [[file:./../images/markarmstrong.jpg]]" /> 11<meta name="description" content="An Agda implementation of a decider for arbitrary predicates 12on the one-point compactification of â." /> 13<meta name="generator" content="Org Mode" /> 14<link rel="stylesheet" type="text/css" href="src/readtheorg_theme/css/htmlize.css"/> 15<link rel="stylesheet" type="text/css" href="src/readtheorg_theme/css/readtheorg.css"/> 16<link rel="stylesheet" type="text/css" href="src/readtheorg_theme/css/search.css"/>
17<script type="text/javascript" src="src/lib/js/jquery.min.js"></script>
vendor: 1 bytes, line 17
17
18<script type="text/javascript" src="src/lib/js/bootstrap.min.js"></script>
vendor: 1 bytes, line 18
18
19<script type="text/javascript" src="src/lib/js/jquery.stickytableheaders.min.js"></script>
vendor: 1 bytes, line 19
19
20<script type="text/javascript" src="src/readtheorg_theme/js/search.js"></script>
vendor: 1 bytes, line 20
20
21<script type="text/javascript" src="src/readtheorg_theme/js/readtheorg.js"></script>
21 22<style>pre.src{background:#000000;color:white;} </style> 23</head> 24<body> 25<div id="content" class="content"> 26<h1 class="title">Decidability in the One-Point Compactification of â</h1> 27<div id="table-of-contents" role="doc-toc"> 28<h2>Table of Contents</h2> 29<div id="text-table-of-contents" role="doc-toc"> 30<ul> 31<li><a href="#Introduction">1. Introduction</a></li> 32<li><a href="#Some-small-extensions-to-the-standard-library">2. Some small extensions to the standard library</a></li> 33<li><a href="#The-one-point-compactification-of-â">3. The one-point compactification of â</a></li> 34<li><a href="#Naming-some-elements-of-~â*~">4. Naming some elements of â*</a></li> 35<li><a href="#The-embedding-of-~â~-into-~â*~">5. The embedding of â into â*</a></li> 36<li><a href="#Decidable-case-checks-on-~â*~">6. Decidable case checks on â*</a></li> 37<li><a href="#Decidability-of-arbitrary-predicates-on-~â*~">7. Decidability of arbitrary predicates on â*</a></li> 38</ul> 39</div> 40</div> 41 42<div id="outline-container-Introduction" class="outline-2"> 43<h2 id="Introduction"><span class="section-number-2">1.</span> Introduction</h2> 44<div class="outline-text-2" id="text-Introduction"> 45<p> 46:TODO: More narrative here. 47</p> 48 49<p> 50From a <a href="https://lists.chalmers.se/pipermail/agda/2020/012150.html">recent Agda mailing list post</a> 51by Martin Escardo. 52</p> 53<blockquote> 54<p> 55We can write the following unlikely functional program in Agda (and in 56Martin-Loef Type Theory of any variety): 57</p> 58 59<p> 60(1) Consider the type of decreasing infinite sequences of digits 0 and 1. 61</p> 62 63<p> 64Call this type ââ, because 65</p> 66 67<ul class="org-ul"> 68<li>The sequence of n-many ones followed by infinitely many zeros 69encodes the natural number n.</li> 70 71<li>The sequence of infinitely many ones encodes â,</li> 72</ul> 73 74<p> 75So we have an embedding â â ââ and a new point â in ââ. 76</p> 77 78<p> 79(2) There is an Agda program that decides, for a given p : ââ â Bool, 80 whether or not there is x : ââ with p x â¡ True. 81</p> 82 83<p> 84Clearly such a program <b>does not</b> exist if we replace ââ by â. 85This non-existence is a theorem of computability theory. 86</p> 87 88<p> 89But it does exist with ââ. 90</p> 91</blockquote> 92</div> 93</div> 94 95<div id="outline-container-Some-small-extensions-to-the-standard-library" class="outline-2"> 96<h2 id="Some-small-extensions-to-the-standard-library"><span class="section-number-2">2.</span> Some small extensions to the standard library</h2> 97<div class="outline-text-2" id="text-Some-small-extensions-to-the-standard-library"> 98<p> 99These I found useful at least at some stage of development 100though I did not end up using all of them. 101They may already be implemented in the standard library, 102just not where I looked; I'd have to double check. 103</p> 104<div class="org-src-container"> 105<pre class="src src-agda2">nothing≢just : <span style="color: #ffffff;">{</span>A : Set<span style="color: #ffffff;">}</span> → <span style="color: #ffffff;">(</span>a : A<span style="color: #ffffff;">)</span> → ¬ <span style="color: #ffffff;">(</span>nothing ≡ just a<span style="color: #ffffff;">)</span> 106nothing≢just a <span style="color: #ffffff;">()</span> 107 108Is-nothing? : <span style="color: #ffffff;">{</span>A : Set<span style="color: #ffffff;">}</span> → <span style="color: #ffffff;">(</span>x : Maybe A<span style="color: #ffffff;">)</span> → Dec <span style="color: #ffffff;">(</span>Is-nothing x<span style="color: #ffffff;">)</span> 109Is-nothing? nothing = yes All.nothing 110Is-nothing? <span style="color: #ffffff;">(</span>just _<span style="color: #ffffff;">)</span> = no λ <span style="color: #ffffff;">{</span> <span style="color: #ff66ff;">(</span>All.just <span style="color: #00eff0;">()</span><span style="color: #ff66ff;">)</span> <span style="color: #ffffff;">}</span> 111 112Is-just? : <span style="color: #ffffff;">{</span>A : Set<span style="color: #ffffff;">}</span> → <span style="color: #ffffff;">(</span>x : Maybe A<span style="color: #ffffff;">)</span> → Dec <span style="color: #ffffff;">(</span>Is-just x<span style="color: #ffffff;">)</span> 113Is-just? nothing = no λ <span style="color: #ffffff;">()</span> 114Is-just? <span style="color: #ffffff;">(</span>just _<span style="color: #ffffff;">)</span> = yes <span style="color: #ffffff;">(</span>Any.just tt<span style="color: #ffffff;">)</span> 115</pre> 116</div> 117</div> 118</div> 119 120<div id="outline-container-The-one-point-compactification-of-â" class="outline-2"> 121<h2 id="The-one-point-compactification-of-â"><span class="section-number-2">3.</span> The one-point compactification of â</h2> 122<div class="outline-text-2" id="text-The-one-point-compactification-of-â"> 123<p> 124First, let us use the name <code>â*</code>, rather than <code>ââ</code>. 125This leads us to naturally append <code>*</code> to the standard names for 126elements of or functions on <code>â*</code>, which is far more readable 127than appending <code>â</code> everywhere. 128We will still call the ânew pointâ of <code>â*</code> <code>â</code>. 129</p> 130 131<p> 132Rather than decreasing infinite sequences of <code>0</code>'s and <code>1</code>'s, 133I choose to represent <code>â*</code> as a potentially infinite string 134of unary constructors; specifically, 135the constructor <code>just</code> of the <code>Maybe</code> type. 136</p> 137<div class="org-src-container"> 138<pre class="src src-agda2">record ℕ* : Set where 139 coinductive 140 field 141 c : Maybe ℕ* 142open ℕ* 143</pre> 144</div> 145 146<p> 147We need to define bisimilarity of elements of <code>â*</code> in order 148to be able to compare them. 149</p> 150<div class="org-src-container"> 151<pre class="src src-agda2">record _≈_ <span style="color: #ffffff;">(</span>m n : ℕ*<span style="color: #ffffff;">)</span> : Set where 152 coinductive 153 field 154 c-≈ : ℕ*.c m ≡ ℕ*.c n 155open _≈_ 156</pre> 157</div> 158 159<p> 160Symmetry and transitivity follow easily. 161</p> 162<div class="org-src-container"> 163<pre class="src src-agda2">≈-sym : <span style="color: #ffffff;">{</span>m n : ℕ*<span style="color: #ffffff;">}</span> → m ≈ n → n ≈ m 164c-≈ <span style="color: #ffffff;">(</span>≈-sym m≈n<span style="color: #ffffff;">)</span> = sym <span style="color: #ffffff;">(</span>c-≈ m≈n<span style="color: #ffffff;">)</span> 165 166≈-trans : <span style="color: #ffffff;">{</span>m n o : ℕ*<span style="color: #ffffff;">}</span> → m ≈ n → n ≈ o → m ≈ o 167c-≈ <span style="color: #ffffff;">(</span>≈-trans m≈n n≈o<span style="color: #ffffff;">)</span> = trans <span style="color: #ffffff;">(</span>c-≈ m≈n<span style="color: #ffffff;">)</span> <span style="color: #ffffff;">(</span>c-≈ n≈o<span style="color: #ffffff;">)</span> 168</pre> 169</div> 170</div> 171</div> 172 173<div id="outline-container-Naming-some-elements-of-~â*~" class="outline-2"> 174<h2 id="Naming-some-elements-of-~â*~"><span class="section-number-2">4.</span> Naming some elements of â*</h2> 175<div class="outline-text-2" id="text-Naming-some-elements-of-~â*~"> 176<p> 177It's convenient to refer to the elements of <code>â*</code> by these more familiar names. 178</p> 179<div class="org-src-container"> 180<pre class="src src-agda2">0* : ℕ* 181c 0* = nothing 182 183suc* : ℕ* → ℕ* 184c <span style="color: #ffffff;">(</span>suc* n<span style="color: #ffffff;">)</span> = just n 185 186∞ : ℕ* 187c ∞ = just ∞ 188</pre> 189</div> 190 191<p> 192Now we provide a series of proofs that these names refer 193to the numbers we have in mind; namely, we want to prove that 194</p> 195<ul class="org-ul"> 196<li>zero is not a successor<sup><a id="fnr.1" class="footref" href="#fn.1" role="doc-backlink">1</a></sup></li> 197<li>successors is an injecive function,</li> 198<li>infinity is a fix-point of successor, and</li> 199<li>infinity is the only fix-point of successor.</li> 200</ul> 201 202<div class="org-src-container"> 203<pre class="src src-agda2">¬<span style="color: #ffffff;">[</span>0*≈suc*-n<span style="color: #ffffff;">]</span> : <span style="color: #ffffff;">(</span>n : ℕ*<span style="color: #ffffff;">)</span> → ¬ 0* ≈ suc* n 204¬<span style="color: #ffffff;">[</span>0*≈suc*-n<span style="color: #ffffff;">]</span> n 0*≈suc*-n = nothing≢just n <span style="color: #ffffff;">(</span>c-≈ 0*≈suc*-n<span style="color: #ffffff;">)</span> 205 206¬<span style="color: #ffffff;">[</span>0*≈∞<span style="color: #ffffff;">]</span> : ¬ <span style="color: #ffffff;">(</span>0* ≈ ∞<span style="color: #ffffff;">)</span> 207¬<span style="color: #ffffff;">[</span>0*≈∞<span style="color: #ffffff;">]</span> 0*≈∞ = nothing≢just ∞ <span style="color: #ffffff;">(</span>c-≈ 0*≈∞<span style="color: #ffffff;">)</span> 208</pre> 209</div> 210 211<div class="org-src-container"> 212<pre class="src src-agda2">suc*-∞≈∞ : suc* ∞ ≈ ∞ 213c-≈ <span style="color: #ffffff;">(</span>suc*-∞≈∞<span style="color: #ffffff;">)</span> = refl 214</pre> 215</div> 216 217<div class="org-src-container"> 218<pre class="src src-agda2">suc*-injective : <span style="color: #ffffff;">{</span>m n : ℕ*<span style="color: #ffffff;">}</span> 219 <span style="color: #533253325332;"> </span> → suc* m ≈ suc* n → m ≈ n 220c-≈ <span style="color: #ffffff;">(</span>suc*-injective m≈n<span style="color: #ffffff;">)</span> = cong c <span style="color: #ffffff;">(</span>just-injective <span style="color: #ff66ff;">(</span>c-≈ m≈n<span style="color: #ff66ff;">)</span><span style="color: #ffffff;">)</span> 221</pre> 222</div> 223 224<div class="org-src-container"> 225<pre class="src src-agda2">¬<span style="color: #ffffff;">[</span>n≈∞<span style="color: #ffffff;">]</span>⇒¬<span style="color: #ffffff;">[</span>suc*-n≈∞<span style="color: #ffffff;">]</span> : <span style="color: #ffffff;">(</span>n : ℕ*<span style="color: #ffffff;">)</span> → ¬ <span style="color: #ffffff;">(</span>n ≈ ∞<span style="color: #ffffff;">)</span> → ¬ <span style="color: #ffffff;">(</span>suc* n ≈ ∞<span style="color: #ffffff;">)</span> 226¬<span style="color: #ffffff;">[</span>n≈∞<span style="color: #ffffff;">]</span>⇒¬<span style="color: #ffffff;">[</span>suc*-n≈∞<span style="color: #ffffff;">]</span> n ¬<span style="color: #ffffff;">[</span>n≈∞<span style="color: #ffffff;">]</span> suc*-n≈∞ = 227 ¬<span style="color: #ffffff;">[</span>n≈∞<span style="color: #ffffff;">]</span> <span style="color: #ffffff;">(</span>suc*-injective <span style="color: #ff66ff;">(</span>≈-trans suc*-n≈∞ 228 <span style="color: #533253325332;"> </span> <span style="color: #533253325332;"> </span> <span style="color: #44843b0e29c3;"> </span> <span style="color: #44843b0e29c3;"> </span> <span style="color: #2a6a396c4cff;"> </span> <span style="color: #2a6a396c4cff;"> </span> <span style="color: #52df381e43dd;"> </span> <span style="color: #52df381e43dd;"> </span> <span style="color: #00eff0;">(</span>≈-sym suc*-∞≈∞<span style="color: #00eff0;">)</span><span style="color: #ff66ff;">)</span><span style="color: #ffffff;">)</span> 229</pre> 230</div> 231</div> 232</div> 233 234<div id="outline-container-The-embedding-of-~â~-into-~â*~" class="outline-2"> 235<h2 id="The-embedding-of-~â~-into-~â*~"><span class="section-number-2">5.</span> The embedding of â into â*</h2> 236<div class="outline-text-2" id="text-The-embedding-of-~â~-into-~â*~"> 237<p> 238Now the embedding of a natural number <code>n</code> into <code>â</code> produces 239a string of <code>just</code>'s of length <code>n</code>, followed by a <code>nothing</code>. 240We could have used our constants here, but we define it 241directly instead. 242</p> 243<div class="org-src-container"> 244<pre class="src src-agda2">embed : ℕ → ℕ* 245embed zero = 0* 246embed <span style="color: #ffffff;">(</span>suc n<span style="color: #ffffff;">)</span> = suc* <span style="color: #ffffff;">(</span>embed n<span style="color: #ffffff;">)</span> 247</pre> 248</div> 249 250<p> 251There is no way that we can obtain the fix-point infinity by embedding. 252</p> 253<div class="org-src-container"> 254<pre class="src src-agda2">¬<span style="color: #ffffff;">[</span>embed-n≈∞<span style="color: #ffffff;">]</span> : <span style="color: #ffffff;">(</span>n : ℕ<span style="color: #ffffff;">)</span> → ¬ <span style="color: #ffffff;">(</span>embed n ≈ ∞<span style="color: #ffffff;">)</span> 255¬<span style="color: #ffffff;">[</span>embed-n≈∞<span style="color: #ffffff;">]</span> zero = ¬<span style="color: #ffffff;">[</span>0*≈∞<span style="color: #ffffff;">]</span> 256¬<span style="color: #ffffff;">[</span>embed-n≈∞<span style="color: #ffffff;">]</span> <span style="color: #ffffff;">(</span>suc n<span style="color: #ffffff;">)</span> = ¬<span style="color: #ffffff;">[</span>n≈∞<span style="color: #ffffff;">]</span>⇒¬<span style="color: #ffffff;">[</span>suc*-n≈∞<span style="color: #ffffff;">]</span> <span style="color: #ffffff;">(</span>embed n<span style="color: #ffffff;">)</span> <span style="color: #ffffff;">(</span>¬<span style="color: #ff66ff;">[</span>embed-n≈∞<span style="color: #ff66ff;">]</span> n<span style="color: #ffffff;">)</span> 257</pre> 258</div> 259</div> 260</div> 261 262<div id="outline-container-Decidable-case-checks-on-~â*~" class="outline-2"> 263<h2 id="Decidable-case-checks-on-~â*~"><span class="section-number-2">6.</span>
263 Decidable case checks on â*</h2> 264<div class="outline-text-2" id="text-Decidable-case-checks-on-~â*~"> 265<p> 266It may be useful for us to be able to distinguish values of <code>â*</code>, 267because we cannot pattern match on elements. 268Decidable <code>Is-zero*</code> and <code>Is-suc*</code> predicates 269allow us to work around that limitation. 270</p> 271<div class="org-src-container"> 272<pre class="src src-agda2">Is-zero* : ℕ* → Set 273Is-zero* = _≈ 0* 274 275Is-suc* : ℕ* → Set 276Is-suc* n = Σ<span style="color: #ffffff;">[</span> m ∈ ℕ* <span style="color: #ffffff;">]</span> n ≈ suc* m 277</pre> 278</div> 279 280<p> 281We can define an <code>Is-â</code> predicate, but unless I miss my mark, 282this cannot be decidable. 283</p> 284<div class="org-src-container"> 285<pre class="src src-agda2">Is-∞ : ℕ* → Set 286Is-∞ = _≈ ∞ 287</pre> 288</div> 289 290<p> 291I cannot see a way around using <code>inspect</code> to define the deciders 292for these. In the <code>no</code> cases, we must somewhat carefully 293constuct the contradictory value. 294</p> 295<div class="org-src-container"> 296<pre class="src src-agda2">Is-zero*? : <span style="color: #ffffff;">(</span>n : ℕ*<span style="color: #ffffff;">)</span> → Dec <span style="color: #ffffff;">(</span>Is-zero* n<span style="color: #ffffff;">)</span> 297Is-zero*? n with c n | inspect c n 298... | nothing | <span style="color: #ffffff;">[</span> c-n≡
298nothing <span style="color: #ffffff;">]</span> = yes <span style="color: #ffffff;">(</span>record <span style="color: #ff66ff;">{</span> c-≈ = c-n≡nothing <span style="color: #ff66ff;">}</span><span style="color: #ffffff;">)</span> 299... | just predn | <span style="color: #ffffff;">[</span> c-n≡just-predn <span style="color: #ffffff;">]</span> = 300 no λ n≈0* → ¬<span style="color: #ffffff;">[</span>0*≈suc*-n<span style="color: #ffffff;">]</span> predn <span style="color: #ffffff;">(</span>≈-sym <span style="color: #ff66ff;">(</span>≈-trans <span style="color: #00eff0;">(</span>record <span style="color: #ff6b55;">{</span> c-≈ = sym c-n≡just-predn <span style="color: #ff6b55;">}</span><span style="color: #00eff0;">)</span> n≈0*<span style="color: #ff66ff;">)</span><span style="color: #ffffff;">)</span> 301</pre> 302</div> 303 304<p> 305:TODO: commentary; I needed these for the approach to <code>Is-suc*?</code> which 306uses <code>Is-zero*?</code>, in order to translate the proofs. 307</p> 308<div class="org-src-container"> 309<pre class="src src-agda2">pred* : <span style="color: #ffffff;">(</span>n : ℕ*<span style="color: #ffffff;">)</span> → ¬ <span style="color: #ffffff;">(</span>Is-zero* n<span style="color: #ffffff;">)</span> → ℕ* 310pred* n ¬Is-zero*-n with c n | inspect c n 311… | nothing | <span style="color: #ffffff;">[</span> c-n≡
311nothing <span style="color: #ffffff;">]</span> = ⊥-elim <span style="color: #ffffff;">(</span>¬Is-zero*-n <span style="color: #ff66ff;">(</span>record <span style="color: #00eff0;">{</span> c-≈ = c-n≡nothing <span style="color: #00eff0;">}</span><span style="color: #ff66ff;">)</span><span style="color: #ffffff;">)</span> 312… | just predn | <span style="color: #ffffff;">[</span> _ <span style="color: #ffffff;">]</span> = predn 313 314suc*-pred* : <span style="color: #ffffff;">(</span>n : ℕ*<span style="color: #ffffff;">)</span> → <span style="color: #ffffff;">(</span>¬Is-zero*-n : ¬ <span style="color: #ff66ff;">(</span>Is-zero* n<span style="color: #ff66ff;">)</span><span style="color: #ffffff;">)</span> 315 <span style="color: #533253325332;"> </span> <span style="color: #533253325332;"> </span> → suc* <span style="color: #ffffff;">(</span>pred* n ¬Is-zero*-n<span style="color: #ffffff;">)</span> ≈ n 316suc*-pred* n ¬Is-zero*-n with c n | inspect c n 317… | nothing | <span style="color: #ffffff;">[</span> c-n≡
317nothing <span style="color: #ffffff;">]</span> = ⊥-elim <span style="color: #ffffff;">(</span>¬Is-zero*-n <span style="color: #ff66ff;">(</span>record <span style="color: #00eff0;">{</span> c-≈ = c-n≡nothing <span style="color: #00eff0;">}</span><span style="color: #ff66ff;">)</span><span style="color: #ffffff;">)</span> 318… | just predn | <span style="color: #ffffff;">[</span> c-n≡just-predn <span style="color: #ffffff;">]</span> = ≈-sym <span style="color: #ffffff;">(</span>record <span style="color: #ff66ff;">{</span> c-≈ = c-n≡just-predn <span style="color: #ff66ff;">}</span><span style="color: #ffffff;">)</span> 319 320¬<span style="color: #ffffff;">[</span>Is-zero*-n<span style="color: #ffffff;">]</span>⇒Is-suc*-n : <span style="color: #ffffff;">(</span>n : ℕ*<span style="color: #ffffff;">)</span> → ¬ <span style="color: #ffffff;">(</span>Is-zero* n<span style="color: #ffffff;">)</span> → Is-suc* n 321¬<span style="color: #ffffff;">[</span>Is-zero*-n<span style="color: #ffffff;">]</span>⇒Is-suc*-n n ¬Is-zero*-n = pred* n ¬Is-zero*-n 322 <span style="color: #533253325332;"> </span> <span style="color: #533253325332;"> </span> <span style="color: #44843b0e29c3;"> </span> <span style="color: #44843b0e29c3;"> </span> <span style="color: #2a6a396c4cff;"> </span> <span style="color: #2a6a396c4cff;"> </span> <span style="color: #52df381e43dd;"> </span> <span style="color: #52df381e43dd;"> </span> <span style="color: #2c5f41e833e0;"> </span> , ≈-sym <span style="color: #ffffff;">(</span>suc*-pred* n ¬Is-zero*-n<span style="color: #ffffff;">)</span> 323</pre> 324</div> 325 326<p> 327It seems natural to decide if a <code>â*</code> is a successor 328by first deciding if it is zero. 329</p> 330<div class="org-src-container"> 331<pre class="src src-agda2">Is-suc*? : <span style="color: #ffffff;">(</span>m : ℕ*<span style="color: #ffffff;">)</span> → Dec <span style="color: #ffffff;">(</span>Is-suc* m<span style="color: #ffffff;">)</span> 332Is-suc*? m = case Is-zero*? m of 333 λ <span style="color: #ffffff;">{</span> <span style="color: #ff66ff;">(</span>yes Is-zero*-m<span style="color: #ff66ff;">)</span> 334 <span style="color: #533253325332;"> </span> → no λ <span style="color: #ff66ff;">{</span> <span style="color: #00eff0;">(</span>n , m≈suc*-n<span style="color: #00eff0;">)</span> → ¬<span style="color: #00eff0;">[</span>0*≈suc*-n<span style="color: #00eff0;">]</span> n <span style="color: #00eff0;">(</span>≈-trans <span style="color: #ff6b55;">(</span>≈-sym Is-zero*-m<span style="color: #ff6b55;">)</span> 335 <span style="color: #533253325332;"> </span> <span style="color: #533253325332;"> </span> <span style="color: #44843b0e29c3;"> </span> <span style="color: #44843b0e29c3;"> </span> <span style="color: #2a6a396c4cff;"> </span> <span style="color: #2a6a396c4cff;"> </span> <span style="color: #52df381e43dd;"> </span> <span style="color: #52df381e43dd;"> </span> <span style="color: #2c5f41e833e0;"> </span> <span style="color: #2c5f41e833e0;"> </span> <span style="color: #5332309d29c3;"> </span> <span style="color: #5332309d29c3;"> </span> <span style="color: #323e41414915;"> </span> <span style="color: #323e41414915;"> </span> m≈suc*-n<span style="color: #00eff0;">)</span> <span style="color: #ff66ff;">}</span> 336 ; <span style="color: #ff66ff;">(</span>no ¬Is-zero*-m<span style="color: #ff66ff;">)</span> → yes <span style="color: #ff66ff;">(</span>¬<span style="color: #00eff0;">[</span>Is-zero*-n<span style="color: #00eff0;">]</span>⇒Is-suc*-n m ¬Is-zero*-m<span style="color: #ff66ff;">)</span> 337 <span style="color: #ffffff;">}</span> 338</pre> 339</div> 340</div> 341</div> 342 343<div id="outline-container-Decidability-of-arbitrary-predicates-on-~â*~" class="outline-2"> 344<h2 id="Decidability-of-arbitrary-predicates-on-~â*~"><span class="section-number-2">7.</span> Decidability of arbitrary predicates on â*</h2> 345<div class="outline-text-2" id="text-Decidability-of-arbitrary-predicates-on-~â*~"> 346<p> 347:TODO: ð 348</p> 349 350<p> 351I had begun a naive approach before I began using bisimilarity above, 352but it quickly got rejected by the termination checker. 353</p> 354 355<p> 356Specifically, it begins by checking <code>p 0*</code>, then if that fails 357it moves on <i>with a modified predicate</i> I called <code>Suc p</code>. 358That works fine, <i>until we examine the result</i> of 359running <code>decide</code> on that predicate. 360</p> 361 362<p> 363All the same, I will likely return to it next, 364unless I suddenly see the correct way forward. 365The current source code is commented out 366in the Org source of this document. 367It needs refactoring, so I don't want to show it yet. 368</p> 369</div> 370</div> 371<div id="footnotes"> 372<h2 class="footnotes">Footnotes: </h2> 373<div id="text-footnotes"> 374 375<div class="footdef"><sup><a id="fn.1" class="footnum" href="#fnr.1" role="doc-backlink">1</a></sup> <div class="footpara" role="doc-footnote"><p class="footpara">From this, we could prove the corollary 376that zero is not infinity, but this would require a use of transitivity, 377so we provide a direct proof.</p></div></div> 378 379 380</div> 381</div></div> 382<div id="postamble" class="status"> 383<p class="author">Author: <a href="https://armkeh.github.io">Mark Armstrong</a> <img src="./../images/markarmstrong.jpg" alt="markarmstrong.jpg" /></p> 384 <p class="author">Contact: <a href="mailto:[email protected]">[email protected]</a></p> 385 <p class="date">Original date: August 25, 2020</p> 386 <p class="date">Last updated: 2024-10-20 Sun 23:33</p> 387 <p class="creator">Created using <a href="https://www.gnu.org/software/emacs/">Emacs</a> 29.4 (<a href="https://orgmode.org">Org</a> mode 9.6.15)</p> 388 <p class="validation"><a href="https://validator.w3.org/check?uri=referer">Validate</a></p> 389</div> 390</body> 391</html>
Line numbers count LF bytes from the start of the resource, as the search results do. Vendor segments are library code the classifier recognised; they are stored but not indexed. Bytes are shown as Latin1 characters, one per byte.