3

I'm working on a problem I stumbled across online. The goal is to define terms for two use cases which are defined as follows:

lists are encoded as:

$ [N_1,N_2,...,N_k] ≜ λc.λn.c N_1 (c N_2 (...(c N_k n)...)) $

$ head [N, . . . ] → _\beta^* N \\ $

$ empty [ ] →_\beta^* true \\ $

$ empty [N, . . . ] →\beta^* false $

With a note that head[] can reduce to whatever I want. Any idea how to define such terms?

gaming4 mining
  • 125

1 Answers1

3

Below, I will write definitions on the form $\mathsf{foo}(x_1,\ldots,x_n)=e$ as syntactic sugar for $\mathsf{foo}=\lambda x_1.\cdots.\lambda x_n.e$ and expressions on the form $\mathsf{foo}(e_1,\ldots,e_n)$ as syntactic sugar for $\mathsf{foo}\ e_1\ \ldots\ e_n$.

List constructors:

  • $\mathsf{nil} = \lambda c.\lambda n.n$
  • $\mathsf{cons}(x,l) = \lambda c.\lambda n.c\ x\ (l\ c\ n)$

By these we have for example $$\begin{align} \mathsf{cons}(N_1, \mathsf{nil}) &= \lambda c.\lambda n.c\ N_1\ (\mathsf{nil}\ c\ n) \to_\beta \lambda c.\lambda n.c\ N_1\ n \\ \mathsf{cons}(N_1, \mathsf{cons}(N_2, \mathsf{nil})) &= \lambda c.\lambda n.c\ N_1\ (\mathsf{cons}(N_2, \mathsf{nil})\ c\ n) \\ &= \lambda c.\lambda n.c\ N_1\ ((\lambda c'.\lambda n'.c'\ N_2\ n')\ c\ n) \\ &\to_\beta \lambda c.\lambda n.c\ N_1\ (c\ N_2\ n) \end{align}$$

To get the head of a list, we need to find some function $c_{\mathsf{head}}$ and some value $n$ such that $\mathsf{cons}(x,l)\ c_{\mathsf{head}}\ n$ reduces to $x$. But $$ \mathsf{cons}(x,l)\ c_{\mathsf{head}}\ n = (\lambda c'.\lambda n'.c'\ x\ (l\ c'\ n'))\ c_{\mathsf{head}}\ n \to_\beta c_{\mathsf{head}}\ x\ (l\ c'\ n) $$ so we see that we can just take $c_{\mathsf{head}} = \lambda x.\lambda r.x$ and the value of $n$ doesn't matter. Therefore, we can take $$ \mathsf{head}(l) = l\ (\lambda x.\lambda r.x)\ \mathsf{id} $$ where $\mathsf{id}(x)=x$.

To check if a list is empty, we need to find some function $c_{\mathsf{empty}}$ and some value $n$ such that $\mathsf{nil}\ c_{\mathsf{empty}}\ n$ reduces to $\mathsf{true}$, while $\mathsf{cons}(x,l)\ c_{\mathsf{empty}}\ n$ reduces to $\mathsf{false}$. But $$ \mathsf{nil}\ c_{\mathsf{empty}}\ n = (\lambda c'.\lambda n'.n')\ c_{\mathsf{empty}}\ n \to_\beta n $$ and $$ \mathsf{cons}(x,l)\ c_{\mathsf{empty}}\ n = (\lambda c'.\lambda n'.c'\ x\ (l\ c'\ n'))\ c_{\mathsf{empty}}\ n \to_\beta c_{\mathsf{empty}}\ x\ (l\ c_{\mathsf{empty}}\ n) . $$ Note that the result for $\mathsf{nil}$ equals $n$ so we can take $n=\mathsf{true}$, and the result for $\mathsf{cons}(x,l)$ is an application of $c_{\mathsf{empty}}$ so we can just let $c_{\mathsf{empty}}\ x\ r$ return $\mathsf{false}.$ We therefore define $$ \mathsf{empty}(l) = l\ (\lambda x.\lambda r.\mathsf{false})\ \mathsf{true} $$

Showing that $\mathsf{head}\ (\mathsf{cons}\ a\ l) \to_\beta^* a$: $$\begin{align} \mathsf{head}\ (\mathsf{cons}\ a\ l) &= (\lambda l'.l'\ (\lambda x.\lambda r.x)\ \mathsf{id})\ (\mathsf{cons}\ a\ l) \\ &\to_\beta (\mathsf{cons}\ a\ l)\ (\lambda x.\lambda r.x)\ \mathsf{id} \\ &= ((\lambda x'.\lambda l'.\lambda c.\lambda n.c\ x'\ (l'\ c\ n))\ a\ l)\ (\lambda x.\lambda r.x)\ \mathsf{id} \\ &= (\lambda x'.\lambda l'.\lambda c.\lambda n.c\ x'\ (l'\ c\ n))\ a\ l\ (\lambda x.\lambda r.x)\ \mathsf{id} \\ &\to_\beta (\lambda l'.\lambda c.\lambda n.c\ a\ (l'\ c\ n))\ l\ (\lambda x.\lambda r.x)\ \mathsf{id} \\ &\to_\beta (\lambda c.\lambda n.c\ a\ (l\ c\ n))\ (\lambda x.\lambda r.x)\ \mathsf{id} \\ &\to_\beta (\lambda n.(\lambda x.\lambda r.x)\ a\ (l\ (\lambda x.\lambda r.x)\ n))\ \mathsf{id} \\ &\to_\beta (\lambda x.\lambda r.x)\ a\ (l\ (\lambda x.\lambda r.x)\ \mathsf{id})) \\ &\to_\beta (\lambda r.a)\ (l\ (\lambda x.\lambda r.x)\ \mathsf{id})) \\ &\to_\beta a \\ \end{align}$$

md2perpe
  • 26,770
  • Hi, thank you for the answer, I'm a bit struggling to interpret the answer. In the head(l)=l (λx.λr.x) id, what is meant by the id? Is it possible to proof that it works by doing something like head([1,2,3] and then reducing it until we get the 1 out? – gaming4 mining Aug 12 '21 at 12:27
  • $\mathsf{id}=\lambda x.x$ But you can pass anything as second argument to $l$ in the definition of $\mathsf{head}$. The second argument isn't really used. – md2perpe Aug 12 '21 at 13:07
  • Try reducing $\mathsf{head}([1,2,3])$ yourself. It's easy, and it will only require a few steps. – md2perpe Aug 12 '21 at 13:11
  • So can we just omit the ID? – gaming4 mining Aug 12 '21 at 13:17
  • Not omit; $l$ needs two arguments. But you can replace it with whatever you want. – md2perpe Aug 12 '21 at 13:19
  • 1
    First step is correct. The rest is incorrect. – md2perpe Aug 12 '21 at 14:01
  • 1
    It's an illegal reduction. You can not reduce $(\lambda n.f\ m\ x\ y\ z)\ a$ to $m\ (x\ y\ z)\ a$. – md2perpe Aug 12 '21 at 14:27
  • What $\lambda$-term do you think that you have applied to what argument when doing your reduction? – md2perpe Aug 12 '21 at 14:31
  • The $\lambda n$ term ends just before $\mathsf{id},$ i.e. you have $(\lambda n.\mathit{something})\ \mathsf{id}$ which $\beta$-reduces to $\mathit{something}[n:=\mathsf{id}]$. – md2perpe Aug 12 '21 at 14:49
  • Apply $(\lambda x.\lambda r.x)$ on $3$. – md2perpe Aug 12 '21 at 15:07
  • 1
    $(\lambda r.3)\ ((\lambda x.\lambda r.x)\ 2\ ((\lambda x.\lambda r.x)\ 1\ \mathsf{id}))$ – md2perpe Aug 12 '21 at 15:28
  • Your parentheses don't match, but after adding the missing ones the calculation looks okay. Note that you could directly have reduced $(\lambda r.3)\ (\ldots)$ to $3$ without first reducing $(\ldots)$. But there are different reduction strategies. – md2perpe Aug 13 '21 at 08:54
  • In my post I have added a reduction of $\mathsf{head}\ (\mathsf{cons}\ a\ l)$ to $a$. There I have used normal order reduction. – md2perpe Aug 13 '21 at 08:56
  • I've found another expression which reduces as well. How is this: $λl.l(λab.a)(any expression)$ different to the solution you've provided in the answer for head ? – gaming4 mining Aug 18 '21 at 13:37
  • @gaming4mining. It's practically the same. The only thing that might differ is the part $(anyexpression)$ that anyway doesn't matter. – md2perpe Aug 18 '21 at 14:35