Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
1 to 4 of 4
I just realized (heh) something interesting. Let $N$ be a “weak natural numbers object” in $Set$, i.e. equipped with an element $z:N$ and a function $s:N\to N$ such that for any set $Y$ with an element $z_Y:Y$ and function $s_Y:N\times Y\to Y$ there exists a not-necessarily-unique function $f:N\to Y$ such that $f(z) = z_X$ and $f(s(x)) = s_Y(x,f(x))$. It follows that $z\neq s(x)$ for all $x:N$, and $s$ is injective. Every “real” natural number $n$ is represented by an element $\mathbf{n} = \overset{n}{\overbrace{s(s(\dots s}}(z)\dots)):N$, but not every element of $N$ need be of this form.
Now work in the realizability tripos of some PCA $A$ in Set (like untyped lambda calculus), so that the predicates over a set $X$ are functons $X\to \Omega = P(A)$. Define a predicate “$x\in \mathbb{N}$” on the set $N$ as follows in the internal tripos logic:
$(x\in \mathbb{N}) \coloneqq \forall (\alpha : N\to \Omega). ((\forall y:N. (\alpha(y) \to \alpha(s(y)))) \to \alpha(z) \to \alpha(x))$That is, $n\in\mathbb{N}$ is the internal assertion that “$n$ satisfies induction”.
Then for any “real” natural number $n$, the Church numeral $\underline{n} = \lambda g k. g^n(k)$ is a realizer of the statement $\mathbf{n}\in\mathbb{N}$. Indeed it is the “obvious” such realizer, corresponding to the obvious way to prove $\mathbf{n}\in\mathbb{N}$: start with the base case $\alpha(z)$ (i.e. the argument $k$), then apply the inductive step (i.e. the argument $g$) $n$ times.
Similarly, if we use the weak recursion principle of $N$ to define operations like $add: N\to N\to N$ and so on, then the Church encodings of the corresponding operations on Church numerals are the “obvious” realizers of the statements that these operations preserve elements satisfying induction. For instance, Church addition $\lambda a b g k. a g(b g k)$ realizes the statement $\forall x y. ((x\in\mathbb{N}) \to (y\in\mathbb{N}) \to (x+y\in\mathbb{N}))$.
This seems like the sort of thing “everyone should know”, but I don’t think I knew it. Did I? Where is it written down? I like it because it connects the use of $\lambda$-calculus as a computational model (where the $\lambda$-terms are the data and the functions that compute with it) to its use in realizability as “witnesses to truth” (where the actual data and functions are in the underlying sets, and the realizers just “track” them), and makes the Church numerals seem unavoidable/canonical in this regard.
I think the first person to note this explicitly was Daniel Leivant in “Reasoning about functional programs and complexity classes associated with type disciplines” (1983) where he explicitly notes that church encoded data can act as proofs of, among other things, induction, connecting them to Kleene Realizability. This idea is used, in a much more generalized form, to generate the datatypes in the more recent Cedille project.
Very interesting; I did not know that before. I idly wonder which statements the Scott numerals realize (see, for instance, page 2 of this set of slides), will think about that.
Thanks! That’s very interesting.
1 to 4 of 4