# λ-Calculus

### Notation

Externally a fairly standard notation is used, as would be familiar to someone using a textbook to study λ-calculus, or as close as we can get without using unicode. I would like to use the unicode 'λ' symbol to represent lambda in FriCAS I/O in many cases this would work fine but there are some consoles and lisps that don't support unicode so, for now, I have held off doing this for maximum compatibility.

I have therefore used the '\' symbol to stand for λ.

Internally the domain stores bound variables using De Bruijn index, in most cases this should not concern the user as I/O uses string names for variables. Converting bound variables internally to index values means that the same variable name can be used, in different lambda terms, without ambiguity and without the need for α-substitution.

De Bruijn index which is a integer where

• 0=inside current (inner) lambda term
• 1= next outer lambda term
• 2= next outer and so on
• ...

We will see how this works in the tutorial below.

So internally the λ-calculus is stored as a binary tree structure using the following syntax:

<term> ::= "\" var "."<term> | n | <term><term> | "("<term>")"

where:

• \ = λ
• n = De Bruijn index which is a integer where, 0=inside inner lambda term, 1= next outer lambda term, 2= next outer and so on.
• var = a string representation of variable (this form is used for unbound variables)
• brackets can be used around whole terms.

## Tutorial

If you are working with a version of FriCAS before 1.1.3 then the Lambda domain needs to be installed on your system, for later versions its already installed. The source code is in a file called computation.spad, which is available here:

Download and compile in the usual way. Make sure it is exposed since Axiom/FriCAS was started.

On this page we will be working with 'untyped' variables so we create an instance called UNTYP to simplify notation:

 ```(1) -> )library VTYP VarTyp is now explicitly exposed in frame frame1 VarTyp will be automatically loaded when needed from /home/martin/VTYP.NRLIB/VTYP (1) -> )library VARCAT VarCat is now explicitly exposed in frame frame1 VarCat will be automatically loaded when needed from /home/martin/VARCAT.NRLIB/VARCAT (1) -> )library UNTYPED Untyped is now explicitly exposed in frame frame1 Untyped will be automatically loaded when needed from /home/martin/UNTYPED.NRLIB/UNTYPED (1) -> )library LAMBDA Lambda is now explicitly exposed in frame frame1 Lambda will be automatically loaded when needed from /home/martin/LAMBDA.NRLIB/LAMBDA (1) -> UNTYP := Lambda Untyped (1) Lambda(Untyped) Type: Type```

### Constructors

First we can enter some variables, at the moment they are not inside a λ-term so they can't yet be bound, but later we can put them into a λ-term..

A numeric name is interpreted as a De Bruijn index when put inside a λ-term, although we don't need this notation for I/O unless we are trying to avoid some ambiguity, because free and bound variables can be constructed by giving the variable name as a string. So in (4) is not yet a vaild term on its own but it will be when put inside a λ-term, when this is done it will be given the name of the bound variable rather than "0".

Internally a string name will be converted to a De Bruijn index when put inside a matching λ-term, otherwise it will be interpreted as a free variable.

 ```(2) -> v1 := lambda(var("x")\$Untyped)\$UNTYP (2) x Type: Lambda(Untyped) (3) -> v2 := lambda(var("y")\$Untyped)\$UNTYP (3) y Type: Lambda(Untyped) (4) -> v3 := lambda(0)\$UNTYP (4) 0 Type: Lambda(Untyped)```

This can be built up into more complex lambda terms by using compound terms (as in (5)) and the λ-term itself (as in (6)).

Each λ-term can only have one bound variable, if more than one bound variable is required then λ-terms can be nested. λ-term requires that the bound variable be given a name.

 ```(5) -> n1 := lambda(v1,v2)\$UNTYP (5) (x y) Type: Lambda(Untyped) (6) -> n2 := lambda(n1,var("x")\$Untyped)\$UNTYP (6) (\x.(x y)) Type: Lambda(Untyped)```

In (7) 'x' is a the bound variable and so, when the λ-term was created, this will be converted to De Bruijn index, in (7) we call toString to see the internal representation:

In (8) we see that when entered as a numeric index the bound variable will still be displayed as a string.

In (9) and (10) we can see that the 'unbind' function can be used to unbind the bound variable 'x' that is, although 'x' has the same string value as the lambda term, it is treated as though it were different. We can see this because the toString output does not have a index value. In (11) we call 'bind' to re-bind it.

 ```(7) -> toString(n2)\$UNTYP (7) (\x.(0 y)) Type: String (8) -> n3 := lambda(v3,var("x")\$Untyped)\$UNTYP (8) (\x.x) Type: Lambda(Untyped) (9) -> u2 := unbind(n2)\$UNTYP (9) (\x.(x y)) Type: Lambda(Untyped) (10) -> toString(u2)\$UNTYP (10) (\x.(x y)) Type: String (11) -> toString(bind(u2))\$UNTYP (11) (\x.(0 y)) Type: String```

So we can already construct any type of lambda term, however its a bit tedious to construct complex lambda terms in this way, an easier way is to use 'parseLambda' to construct the lambda term from a string. Again we can enter variables as either alpha or numeric characters depending on whether we want to specify the index value directly or allow the code to generate it.

In (14) we can see the use of numeric terms to avoid the ambiguity caused by nested λ-terms with the same name.

 ```(12) -> n4 := parseLambda("\x.\y. y x")\$UNTYP (12) (\x.(\y.(x y))) Type: Lambda(Untyped) (13) -> toString(n4)\$UNTYP (13) (\x.(\y.(0 1))) Type: String (14) -> n4a := parseLambda("\x.\x. 0 1")\$UNTYP (14) (\x.(\x'.(x x'))) Type: Lambda(Untyped) (15) -> toString(n4a)\$UNTYP (15) (\x.(\x.(0 1))) Type: String (16) -> unbind(n4a)\$UNTYP (16) (\x.(\x'.(x x))) Type: Lambda(Untyped)```

### β-substitution

The command: subst:(n,a,b) substitutes 'a' for 'b' in 'n' as follows:

 ```(17) -> subst(n2,v2,v1)\$UNTYP (17) (\x.(x y)) Type: Lambda(Untyped) (18) -> subst(n2,v1,v2)\$UNTYP (18) (\x.(x x)) Type: Lambda(Untyped)```

### Issues

I realise that Axiom/FriCAS already has a way to create anonymous functions using +-> in a λ-calculus sort of way. But the aim here is to represent λ-calculus as a pure mathematical structure so that we can experiment with the properties of this structure without the messy features that are required for a practical computer language. I also need a domain structure which is related to SKI combinators and IntuitionisticLogic domain and can be coerced to and from these other domain types as demonstrated on this page.

I also realise that this is written in SPAD which is written in Lisp which is based on λ-Calculus (perhaps it could later be optimised by having direct calls to Lisp?)

### Relationship to Other Domains

λ-calculus can be coerced to and from SKI combinators. For a tutorial about how to coerce to/from this algebra see this page.