# Indexing a list in Lambda calculus

I have tried to implement a list indexing function in lambda calculus and for some reason it is not working. Would anyone be able to point out to me what I am doing wrong? Assuming standard church encoding for numerals. Thank you.

nil = \c.\n.n

cons = \h.\t.\c.\n.c h (t c n)

identity = \x. x

# Example

list = cons 4 (cons 2 (cons 2 (cons 3 nil)))

• should become list = \c.\n. c 4 (c 2 (c 2 ( c 3 (n))))

index = \l. \n. true (n(false l identity 0))

index list 2

• should become true (2(false 4 (2 (2 (3 (0))))) = true (false(false(4 (2 (2 (3 (0))))) = true (false (2 (2 (3 (0))) = true (2 (3 (0)) = 2
• What do you mean by indexing a list? I can’t tell from the example alone Commented Apr 12 at 13:21
• @confusedcius access an element at given index n Commented Apr 12 at 22:24

Recall that a Church numeral $$n$$ is $$λf.λx. f^n x$$. When given arguments, it applies $$f$$ to $$x$$ $$n$$ times.

So to index a list, we can apply the tail function to the list n-1 times, then get the head of the list. Assuming the list is 0-indexed, we can just use the index i to apply the tail i times.

$$index := λl.\ λi.\ head\ (i\ tail\ l)$$

For example, $$list := λc.λn.\ c\ 2\ (c\ 5\ (c\ 3\ n)) = [2;5;3]\\ index\ list\ 1 \rightarrow head\ (1\ tail\ list)\\ \rightarrow head\ (1\ tail\ (λc.λn.\ c\ 2\ (c\ 5\ (c\ 3\ n)))) \\ \rightarrow head\ (tail\ (λc.λn.\ c\ 2\ (c\ 5\ (c\ 3\ n)))) \\ \rightarrow head\ (λc.λn.\ c\ 5\ (c\ 3\ n)) \\ \rightarrow 5 \\\\$$ Both $$head$$ and $$tail$$ returns $$nil$$ when the list is $$nil$$, so this function returns $$nil$$ if the index is out of bound.

In your attempt, note that true is $$λa.λb. a$$, so $$true\ (2\ (3\ (0)) = λb. (2\ (3\ (0))$$, and not $$2$$ (and there are similar errors in other steps).

• But what are the head and tail functions? Commented Apr 15 at 4:22
• @Fraser Oh I assumed they’d be given since they’re usually more important than other list functions. Head returns the first element, tail returns the list without the first element Commented Apr 15 at 4:55
• But how do you implement those? second = \x. false x tail = \l. \c. \n. second (l c n) Commented Apr 15 at 5:49
• @Fraser head is pretty straightforward but how to implement tail is not obvious. See en.m.wikipedia.org/wiki/Church_encoding (list encoding section, right fold) Commented Apr 15 at 13:21
• Btw your implementation doesn’t work for the same reason. You seem to be making the same mistake again. You should write out an example, and make sure you write down parentheses Commented Apr 15 at 13:23