9/17/19
We are going to want to deal with lists, numbers, and suchlike. To do this we have to choose representations. Let me warn you that some of this is going to appear too too clever (this is not my doing). It is also not unique. There are many different ways of doing this, all of which achieve the same ends.
For lists we will need a constructor, an empty list, accessors for the head and tail, and a predicate to tell us whether a list is empty.
With data structures for lists, typically it is all done by means of pairing (that is the constructor) and something for an empty list. So, at the level of hand waving, we might have {} for the empty list. Then if we want a list containing the one item 'a' we pair 'a' with the empty list, thus
pair[a,{}] (*which is {a} *)
and if we want a list with two elements b, a in that order, ie {b a} we pair b with the list we already have containing just 'a', thus
pair[b, pair[a,{}]] (*which is {b a} *)
This is familiar from the programming language LISP, where the pairing constructor is CONS.
Each time a new item is paired in to form a new extended list, the new item is the head of the list and old list, in its entirety, is the tail of the new list.
Our accessors (for head and for tail) are going to need to access the first item of the pair, and the second item of the pair, respectively. But we have already seen something like this, namely true and false
λx.λy.x (*TRUE*)
λx.λy.y (*FALSE*)
it may be, with the right representation, we can use these as the accessors for lists,
λx.λy.x (*HEAD or FIRST*)
λx.λy.y (*TAIL or SECOND*)
If we remember how IF-THEN-ELSE works, it applies TRUE (or FALSE) to the arguments, and then the TRUE (or FALSE) do the selection. We can do a similar thing with lists, we can use a function that passes the accessor as the pairing glue, thus
λpairAccessor.((pairAccessor firstArg) secondArg)
Then, when this is applied to an accessor, it works appropriately eg
(λpairAccessor.((pairAccessor firstArg) secondArg) λx.λy.x)
(( λx.λy.x firstArg) secondArg)
(λy.firstArg secondArg)
firstArg
One oddity on first encounter is the question of which function is applied to which arguments. Ordinarily we think of a list, L say, and an accessor, Head say, and we applied the accessor Head to the list L to get what we want. But here this is working the other way around, we apply the Pair (or List) to the accessor to get what we want.
Thus far we have worked with pairs, or a pair, as a given. But we haven't given any attention to constructing or creating a pair in the first place. But that is easily done
λfirstArg.λsecondArg.λpairAccessor.((pairAccessor firstArg) secondArg) (*PAIR CONSTRUCTOR*)
When this is applied to two arguments (two single arguments in turn), it will swallow both of them and return
λpairAccessor.((pairAccessor firstArg) secondArg)
which is what we want.
Do try some yourself
a) (λpairAccessor.((pairAccessor firstArg) secondArg) λx.λy.x)⇒firstArg (*accessing the first element of a pair*)
b) (λpairAccessor.((pairAccessor firstArg) secondArg) λx.λy.y)⇒ secondArg (*accessing the second element of a pair *)
c)(((λf.λs.λacc.((acc f) s) hello) goodbye) λx.λy.x)⇒hello *(making a pair out of hello goodbye and then accessing the first one*)
So the representation for a pair is
λpairAccessor.((pairAccessor firstArg) secondArg) (*A PAIR*)
or, more briefly
λa.((a h) t) (*A PAIR*)
We can make lists out of this, once we have a representation for the empty list. And, in turn, that representation is motivated by the predicate (or test) for a list being empty.
[In what follows we are using lower case 't' as a mnemonic for 'tail' and the upper case 'T' is our defined expression for 'true' given above.]
The empty list NIL is defined to be
λx.T (* NIL *)
this is so that the empty predicate (the predicate which tests whether a list is empty) can be defined neatly
λlist.(list λh.λt.F) (* NULLQ -- the empty list predicate *)
If this is applied to NIL we get
(λlist.(list λh.λt.F) λx.T)
(λx.T λh.λt.F)
T
which is what we want (the test for an empty list is applied to the empty list and it returns TRUE).
Any non empty list is going to consist of λa.((a h) t) of the head and the tail of that list paired together. If we apply the test predicate NULLQ to an expression of this form we get
(λlist.(list λh.λt.F) λa.((a h) t)
(λa.((a h) t) λh.λt.F)
((λh.λt.F h) t)
(λt.F t)
F
which is what we want (the test for an empty list is applied to a non-empty list and it returns FALSE).
To review lists:-
λx.T (* NIL *)
λlist.(list λh.λt.F) (* NULLQ -- the empty list predicate *)
λa.((a h) t) (*A LIST WITH HEAD h AND TAIL h)*)
λh.λt.λa.((a h) t) (*A CONSTRUCTOR TO MAKE A LIST WITH HEAD h AND TAIL t*)
λx.λy.x (*AN ACCESSOR FOR HEAD*)
λx.λy.y (*AN ACCESSOR FOR TAIL*)
So, using some informal notation, if {} is the empty list and {one,two,three} is the list of one, two and three, then, as examples, within lambda calculus, with our conventions, these lists would be
λx.T
and
λa.((a one) λa.((a two) λa.((a three) λx.T)))
respectively.
Try this exercise
a) (λa.((a one) λa.((a two) λa.((a three) λx.T))) λx.λy.x)⇒one (*the head of the list {a,b,c} is a*)
b) (λa.((a one) λa.((a two) λa.((a three) λx.T))) λx.λy.y)⇒λa.((a two) λa.((a three) λx.T)) (*the tail of the list {one,two,three} is the list {two,three}*)
Numbers
For numbers we also need a representation. There are a variety of different ways of doing numerals or numbers. Usually an expression is chosen to be zero, then some function applied to that to get 1, then then same function applied to that to get 2, and so on... So, in effect, numerals are iterated function applications. We can do this with lists.
For our purposes we need the positive integers:- 0, successor, and predecessor.
Let us represent the number n by a n-element list of any objects, in which case 0 is just NIL, EQ0 is NULLQ, PRED is TAIL. We actually don't care what is in the lists, as long as there is n of them. But to be definite we could say that we will put 0 in the lists-- so the number 0 is NIL, the number 1 is {0} the number 2 is {0, 0} and so on...
λx.T (*0 (also NIL) *)
λlist.(list λhλt.F) (* EQ0 (also NULLQ)*)
λx.λy.y (*PREDECESSOR (also AN ACCESSOR FOR TAIL)*)
to get successor all we have to do is cons or pair 0 on the front of the number as the new head.
λt.λa.((a 0) t) (*SUCCESSOR (also A CONSTRUCTOR TO MAKE A LIST WITH HEAD 0 AND TAIL t)*)