2
$\begingroup$

I'm reading a book on the $\lambda$-calculus and I'm stuck on a list of representations. While practising different lambda calculus tasks I've stumbled upon an interesting issue. Given two terms I would like to understand what list is represented by those - or what is the actual process of transforming those.

I have two terms defined:

$F_n$ and $F'_n$ for each natural number $n \in \mathbb{N} $ is defined as following:

  • $n$ is either a number or a Church encoding,
  • $m$ and $c$ are variables.

$F'_0 = m$

$F'_n = c n F'_{n-1}$ for $n > 0$

$F_n =\lambda c. \lambda m.F'_n $

The question is what kind of list does the term $F_n$ represent?

Expanding a bit on the question as the context was marked as insufficient. Understanding how different lists are represented in lambda calculus is an important part of a learning process, moreover, I haven't found any great sources on how in the general process given terms into a specific list type. The provided answer nicely highlights the process of transitioning a term into an actual list representation.

$\endgroup$

1 Answer 1

Reset to default
4
$\begingroup$

To understand the meaning of a family of terms defined by induction, my suggestion is to take some concrete examples. So, let us see what are $F_0'$, $F_1'$, $F_2'$, $F_3'$, and $F_0$, $F_1$, $F_2$, $F_3$ (for every $n \in \mathbb{N}$, the Church numeral representing $n$ is denoted by $\underline{n}$)

\begin{align} F_0' &= m & F_0 &= \lambda c. \lambda m. m \\ F_1' &= c \underline{1} F_0' = c \, \underline{1} \, m & F_1 &= \lambda c. \lambda m. c \, \underline{1} \, F_0' = \lambda c. \lambda m. c \, \underline{1} \, m \\ F_2' &= c \, \underline{2} \, F_1' = c \,\underline{2} (c \,\underline{1} \, m ) & F_2 &= \lambda c. \lambda m. c \,\underline{2} \, F_1' = \lambda c. \lambda m. c \, \underline{2} (c \, \underline{1} \, m ) \\ F_3' &= c \, \underline{3} \, F_2' = c \, \underline{3} (c \, \underline{2} (c \, \underline{1} \, m )) & F_3 &= \lambda c. \lambda m. c \, \underline{3} \, F_2' = \lambda c. \lambda m. c \, \underline{3} (c \, \underline{2} (c \, \underline{1} \, m )) \\ \dots & & \dots \\ F_n' &= c \, \underline{n} \, F_{n-1}' = c \, \underline{n} (c \,\underline{n\!-\!1} \dots(c \, \underline{1} \, m )) & F_n &= \lambda c. \lambda m. c \, \underline{n} \, F_{n-1}' = \lambda c. \lambda m. c \, \underline{n} (c \,\underline{n\!-\!1} \dots(c \, \underline{1} \, m )) \end{align}

Now, as explained here and here, a list $[M_1, \dots, M_n]$ of $n \in \mathbb{N}$ "objects" can be represented in the $\lambda$-calculus by the term $$\tag{$*$} \lambda c.\lambda m.c M_1 (c M_2 (\dots(c M_n m)...)) $$ Comparing $(*)$ and $F_n$, it is clear that $F_n$ is nothing but the instance of $(*)$ where $M_1$ is replaced by $\underline{n}$, and $M_2$ is replaced by $\underline{n-1}$, and so on (in general, $M_k$ is replaced by $\underline{n-k+1}$, for all $1 \leq k \leq n$). Therefore, for every $n \in \mathbb{N}$, the term $$F_n = \lambda c. \lambda m. c \, \underline{n} (c \,\underline{n\!-\!1} \dots(c \, \underline{1} \, m ))$$ represents $$[\,\underline{n}, \underline{n-1}, \dots, \underline{1}\,]$$ the decreasing list of natural numbers from $n$ to $1$.

$\endgroup$
5
  • $\begingroup$ Thank you for the answer, I was thinking would it be possible to proof that by induction somewhat like: $F'_n[times/c,1/n] →_\beta^* n! $ thus $F_n times 1 →_\beta^* n!$ where ! is factorial and $times \ a \ b$ reduces to $a * b$? $\endgroup$ Commented Aug 15, 2021 at 12:09
  • 1
    $\begingroup$ @gaming4mining - Yes, absolutely. This is essentially the way the function $\mathsf{foldr}$ works in Haskell. $\endgroup$ Commented Aug 15, 2021 at 12:23
  • $\begingroup$ How would the induction proof look like? I can't seem to be getting the correct result. $\endgroup$ Commented Aug 15, 2021 at 12:35
  • 1
    $\begingroup$ @gaming4mining - I guess you can prove that $F_n'[\mathsf{times}/c, \underline{1}/m] \to_\beta^* n!$ by straightforward induction on $n \in \mathbb{N}$. If you have trouble with this proof, please ask a question in a new post, to keep the site tidy. $\endgroup$ Commented Aug 15, 2021 at 13:19
  • $\begingroup$ I've posted the questiom here: link, however I'm not sure if I shouldn't edit this question instead, because the contents of it depends on given solution to this one. $\endgroup$ Commented Aug 15, 2021 at 20:18

You must log in to answer this question.

Start asking to get answers

Find the answer to your question by asking.

Ask question

Explore related questions

See similar questions with these tags.