PageSourceSearch

https://armkeh.github.io/blog/DecidabilityInACompactificationOfNat.html

html armkeh.github.io collected 2026-10-03 08:39:18 UTC 25,234 bytes, 391 lines download raw bytes

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&#8802;just : <span style="color: #ffffff;">{</span>A : Set<span style="color: #ffffff;">}</span> &#8594; <span style="color: #ffffff;">(</span>a : A<span style="color: #ffffff;">)</span> &#8594; &#172; <span style="color: #ffffff;">(</span>nothing &#8801; just a<span style="color: #ffffff;">)</span>
106nothing&#8802;just a <span style="color: #ffffff;">()</span>
107
108Is-nothing? : <span style="color: #ffffff;">{</span>A : Set<span style="color: #ffffff;">}</span> &#8594; <span style="color: #ffffff;">(</span>x : Maybe A<span style="color: #ffffff;">)</span> &#8594; 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 &#955; <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> &#8594; <span style="color: #ffffff;">(</span>x : Maybe A<span style="color: #ffffff;">)</span> &#8594; Dec <span style="color: #ffffff;">(</span>Is-just x<span style="color: #ffffff;">)</span>
113Is-just? nothing = no &#955; <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 &#8469;* : Set where
139  coinductive
140  field
141    c : Maybe &#8469;*
142open &#8469;*
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 _&#8776;_ <span style="color: #ffffff;">(</span>m n : &#8469;*<span style="color: #ffffff;">)</span> : Set where
152  coinductive
153  field
154    c-&#8776; : &#8469;*.c m &#8801; &#8469;*.c n
155open _&#8776;_
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">&#8776;-sym : <span style="color: #ffffff;">{</span>m n : &#8469;*<span style="color: #ffffff;">}</span> &#8594; m &#8776; n &#8594; n &#8776; m
164c-&#8776; <span style="color: #ffffff;">(</span>&#8776;-sym m&#8776;n<span style="color: #ffffff;">)</span> = sym <span style="color: #ffffff;">(</span>c-&#8776; m&#8776;n<span style="color: #ffffff;">)</span>
165
166&#8776;-trans : <span style="color: #ffffff;">{</span>m n o : &#8469;*<span style="color: #ffffff;">}</span> &#8594; m &#8776; n &#8594; n &#8776; o &#8594; m &#8776; o
167c-&#8776; <span style="color: #ffffff;">(</span>&#8776;-trans m&#8776;n n&#8776;o<span style="color: #ffffff;">)</span> = trans <span style="color: #ffffff;">(</span>c-&#8776; m&#8776;n<span style="color: #ffffff;">)</span> <span style="color: #ffffff;">(</span>c-&#8776; n&#8776;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* : &#8469;*
181c 0* = nothing
182
183suc* : &#8469;* &#8594; &#8469;*
184c <span style="color: #ffffff;">(</span>suc* n<span style="color: #ffffff;">)</span> = just n
185
186&#8734; : &#8469;*
187c &#8734; = just &#8734;
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">&#172;<span style="color: #ffffff;">[</span>0*&#8776;suc*-n<span style="color: #ffffff;">]</span> : <span style="color: #ffffff;">(</span>n : &#8469;*<span style="color: #ffffff;">)</span> &#8594; &#172; 0* &#8776; suc* n
204&#172;<span style="color: #ffffff;">[</span>0*&#8776;suc*-n<span style="color: #ffffff;">]</span> n 0*&#8776;suc*-n = nothing&#8802;just n <span style="color: #ffffff;">(</span>c-&#8776; 0*&#8776;suc*-n<span style="color: #ffffff;">)</span>
205
206&#172;<span style="color: #ffffff;">[</span>0*&#8776;&#8734;<span style="color: #ffffff;">]</span> : &#172; <span style="color: #ffffff;">(</span>0* &#8776; &#8734;<span style="color: #ffffff;">)</span>
207&#172;<span style="color: #ffffff;">[</span>0*&#8776;&#8734;<span style="color: #ffffff;">]</span> 0*&#8776;&#8734; = nothing&#8802;just &#8734; <span style="color: #ffffff;">(</span>c-&#8776; 0*&#8776;&#8734;<span style="color: #ffffff;">)</span>
208</pre>
209</div>
210
211<div class="org-src-container">
212<pre class="src src-agda2">suc*-&#8734;&#8776;&#8734; : suc* &#8734; &#8776; &#8734;
213c-&#8776; <span style="color: #ffffff;">(</span>suc*-&#8734;&#8776;&#8734;<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 : &#8469;*<span style="color: #ffffff;">}</span>
219    <span style="color: #533253325332;"> </span> &#8594; suc* m &#8776; suc* n &#8594; m &#8776; n
220c-&#8776; <span style="color: #ffffff;">(</span>suc*-injective m&#8776;n<span style="color: #ffffff;">)</span> = cong c <span style="color: #ffffff;">(</span>just-injective <span style="color: #ff66ff;">(</span>c-&#8776; m&#8776;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">&#172;<span style="color: #ffffff;">[</span>n&#8776;&#8734;<span style="color: #ffffff;">]</span>&#8658;&#172;<span style="color: #ffffff;">[</span>suc*-n&#8776;&#8734;<span style="color: #ffffff;">]</span> : <span style="color: #ffffff;">(</span>n : &#8469;*<span style="color: #ffffff;">)</span> &#8594; &#172; <span style="color: #ffffff;">(</span>n &#8776; &#8734;<span style="color: #ffffff;">)</span> &#8594; &#172; <span style="color: #ffffff;">(</span>suc* n &#8776; &#8734;<span style="color: #ffffff;">)</span>
226&#172;<span style="color: #ffffff;">[</span>n&#8776;&#8734;<span style="color: #ffffff;">]</span>&#8658;&#172;<span style="color: #ffffff;">[</span>suc*-n&#8776;&#8734;<span style="color: #ffffff;">]</span> n &#172;<span style="color: #ffffff;">[</span>n&#8776;&#8734;<span style="color: #ffffff;">]</span> suc*-n&#8776;&#8734; =
227  &#172;<span style="color: #ffffff;">[</span>n&#8776;&#8734;<span style="color: #ffffff;">]</span> <span style="color: #ffffff;">(</span>suc*-injective <span style="color: #ff66ff;">(</span>&#8776;-trans suc*-n&#8776;&#8734;
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>&#8776;-sym suc*-&#8734;&#8776;&#8734;<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 : &#8469; &#8594; &#8469;*
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">&#172;<span style="color: #ffffff;">[</span>embed-n&#8776;&#8734;<span style="color: #ffffff;">]</span> : <span style="color: #ffffff;">(</span>n : &#8469;<span style="color: #ffffff;">)</span> &#8594; &#172; <span style="color: #ffffff;">(</span>embed n &#8776; &#8734;<span style="color: #ffffff;">)</span>
255&#172;<span style="color: #ffffff;">[</span>embed-n&#8776;&#8734;<span style="color: #ffffff;">]</span> zero = &#172;<span style="color: #ffffff;">[</span>0*&#8776;&#8734;<span style="color: #ffffff;">]</span>
256&#172;<span style="color: #ffffff;">[</span>embed-n&#8776;&#8734;<span style="color: #ffffff;">]</span> <span style="color: #ffffff;">(</span>suc n<span style="color: #ffffff;">)</span> = &#172;<span style="color: #ffffff;">[</span>n&#8776;&#8734;<span style="color: #ffffff;">]</span>&#8658;&#172;<span style="color: #ffffff;">[</span>suc*-n&#8776;&#8734;<span style="color: #ffffff;">]</span> <span style="color: #ffffff;">(</span>embed n<span style="color: #ffffff;">)</span> <span style="color: #ffffff;">(</span>&#172;<span style="color: #ff66ff;">[</span>embed-n&#8776;&#8734;<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* : &#8469;* &#8594; Set
273Is-zero* = _&#8776; 0*
274
275Is-suc* : &#8469;* &#8594; Set
276Is-suc* n = &#931;<span style="color: #ffffff;">[</span> m &#8712; &#8469;* <span style="color: #ffffff;">]</span> n &#8776; 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-&#8734; : &#8469;* &#8594; Set
286Is-&#8734; = _&#8776; &#8734;
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 : &#8469;*<span style="color: #ffffff;">)</span> &#8594; 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&#8801;
298nothing <span style="color: #ffffff;">]</span> = yes <span style="color: #ffffff;">(</span>record <span style="color: #ff66ff;">{</span> c-&#8776; = c-n&#8801;nothing <span style="color: #ff66ff;">}</span><span style="color: #ffffff;">)</span>
299... | just predn | <span style="color: #ffffff;">[</span> c-n&#8801;just-predn <span style="color: #ffffff;">]</span>  =
300  no &#955; n&#8776;0* &#8594; &#172;<span style="color: #ffffff;">[</span>0*&#8776;suc*-n<span style="color: #ffffff;">]</span> predn <span style="color: #ffffff;">(</span>&#8776;-sym <span style="color: #ff66ff;">(</span>&#8776;-trans <span style="color: #00eff0;">(</span>record <span style="color: #ff6b55;">{</span> c-&#8776; = sym c-n&#8801;just-predn <span style="color: #ff6b55;">}</span><span style="color: #00eff0;">)</span> n&#8776;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 : &#8469;*<span style="color: #ffffff;">)</span> &#8594; &#172; <span style="color: #ffffff;">(</span>Is-zero* n<span style="color: #ffffff;">)</span> &#8594; &#8469;*
310pred* n &#172;Is-zero*-n with c n | inspect c n
311&#8230; | nothing | <span style="color: #ffffff;">[</span> c-n&#8801;
311nothing <span style="color: #ffffff;">]</span> = &#8869;-elim <span style="color: #ffffff;">(</span>&#172;Is-zero*-n <span style="color: #ff66ff;">(</span>record <span style="color: #00eff0;">{</span> c-&#8776; = c-n&#8801;nothing <span style="color: #00eff0;">}</span><span style="color: #ff66ff;">)</span><span style="color: #ffffff;">)</span>
312&#8230; | just predn | <span style="color: #ffffff;">[</span> _ <span style="color: #ffffff;">]</span> = predn
313
314suc*-pred* : <span style="color: #ffffff;">(</span>n : &#8469;*<span style="color: #ffffff;">)</span> &#8594; <span style="color: #ffffff;">(</span>&#172;Is-zero*-n : &#172; <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>  &#8594; suc* <span style="color: #ffffff;">(</span>pred* n &#172;Is-zero*-n<span style="color: #ffffff;">)</span> &#8776; n
316suc*-pred* n &#172;Is-zero*-n with c n | inspect c n
317&#8230; | nothing | <span style="color: #ffffff;">[</span> c-n&#8801;
317nothing <span style="color: #ffffff;">]</span> = &#8869;-elim <span style="color: #ffffff;">(</span>&#172;Is-zero*-n <span style="color: #ff66ff;">(</span>record <span style="color: #00eff0;">{</span> c-&#8776; = c-n&#8801;nothing <span style="color: #00eff0;">}</span><span style="color: #ff66ff;">)</span><span style="color: #ffffff;">)</span>
318&#8230; | just predn | <span style="color: #ffffff;">[</span> c-n&#8801;just-predn <span style="color: #ffffff;">]</span> = &#8776;-sym <span style="color: #ffffff;">(</span>record <span style="color: #ff66ff;">{</span> c-&#8776; = c-n&#8801;just-predn <span style="color: #ff66ff;">}</span><span style="color: #ffffff;">)</span>
319
320&#172;<span style="color: #ffffff;">[</span>Is-zero*-n<span style="color: #ffffff;">]</span>&#8658;Is-suc*-n : <span style="color: #ffffff;">(</span>n : &#8469;*<span style="color: #ffffff;">)</span> &#8594; &#172; <span style="color: #ffffff;">(</span>Is-zero* n<span style="color: #ffffff;">)</span> &#8594; Is-suc* n
321&#172;<span style="color: #ffffff;">[</span>Is-zero*-n<span style="color: #ffffff;">]</span>&#8658;Is-suc*-n n &#172;Is-zero*-n = pred* n &#172;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>  , &#8776;-sym <span style="color: #ffffff;">(</span>suc*-pred* n &#172;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 : &#8469;*<span style="color: #ffffff;">)</span> &#8594; Dec <span style="color: #ffffff;">(</span>Is-suc* m<span style="color: #ffffff;">)</span>
332Is-suc*? m = case Is-zero*? m of
333  &#955; <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>   &#8594; no &#955; <span style="color: #ff66ff;">{</span> <span style="color: #00eff0;">(</span>n , m&#8776;suc*-n<span style="color: #00eff0;">)</span> &#8594; &#172;<span style="color: #00eff0;">[</span>0*&#8776;suc*-n<span style="color: #00eff0;">]</span> n <span style="color: #00eff0;">(</span>&#8776;-trans <span style="color: #ff6b55;">(</span>&#8776;-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&#8776;suc*-n<span style="color: #00eff0;">)</span> <span style="color: #ff66ff;">}</span>
336    ; <span style="color: #ff66ff;">(</span>no &#172;Is-zero*-m<span style="color: #ff66ff;">)</span> &#8594; yes <span style="color: #ff66ff;">(</span>&#172;<span style="color: #00eff0;">[</span>Is-zero*-n<span style="color: #00eff0;">]</span>&#8658;Is-suc*-n m &#172;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.