Difference between revisions of "Notes:Lambda calculus"

From Maths
Jump to: navigation, search
(Saving progress so far)
 
m
Line 4: Line 4:
 
We define {{lambda|terms}} as follows:<ref name="LCAC">Lambda Calculus and Combinators, an introduction, J. Roger Hindley and Jonathan P. Seldin</ref><br/>
 
We define {{lambda|terms}} as follows:<ref name="LCAC">Lambda Calculus and Combinators, an introduction, J. Roger Hindley and Jonathan P. Seldin</ref><br/>
 
Let the following be given:
 
Let the following be given:
* ''Variables'': an infinite [[sequence]] of expressions, {{M|v_1,\cdots,v_n\cdots}} <ref group="Note">The book uses {{M|v_0,v_{00},v_{000},\cdots}} for some yet unknown reason</ref>
+
* ''Variables'': an infinite [[sequence]] of expressions, {{M|v_1,\ldots,v_n\ldots}} <ref group="Note">The book uses {{M|v_0,v_{00},v_{000},\cdots}} for some yet unknown reason</ref>
 
* ''Atomic constants'': a sequence of expressions again, that may also be finite or empty
 
* ''Atomic constants'': a sequence of expressions again, that may also be finite or empty
 
The set of expressions called ''{{lambda|terms}}'' is defined inductively as follows:
 
The set of expressions called ''{{lambda|terms}}'' is defined inductively as follows:
Line 16: Line 16:
 
===Examples===
 
===Examples===
 
* {{M|(\lambda v_0.(v_0v_{00}))}} - a function that {{M|x\mapsto x(v_{00})}} I think
 
* {{M|(\lambda v_0.(v_0v_{00}))}} - a function that {{M|x\mapsto x(v_{00})}} I think
 +
Here {{M|x}}, {{M|y}} and {{M|z}} are distinct variables:
 +
* {{M|(\lambda x.(xy))}} - a function that {{M|x\mapsto x(y)}} I think
 +
* {{M|((\lambda y.y)(\lambda x.(xy)))}} - This is difficult to put into words, but simply results in the function that {{M|x\mapsto x(y)}}
 +
* {{M|(x(\lambda x.(\lambda x.x)))}} - This is nasty, it looks like {{M|x(x)}}
 +
* {{M|(\lambda x.(yz))}} 'constant' function that {{M|x\mapsto y(z)}}
 +
===Notations===
 +
* Capital letters denote arbitrary {{lambda}} terms
 +
* {{M|x,y,z,u,v,w}} will denote variables
 +
* Brackets will be skipped where it is understood that things are left associative, that is:
 +
** {{M|MNPQ}} is understood to mean {{M|(((MN)P)Q)}} (which to us means: {{M|((M(N))(P))(Q)}} - you can see why this notation is dropped!)
 +
* {{M|(\lambda x.(PQ))}} will become {{M|\lambda x.PQ}}
 +
* {{M|(\lambda x_1.(\lambda x_2.(\ldots(\lambda x_n.M)\ldots))).}} becomes {{M|\lambda x_1x_2\ldots x_n.M}}
 +
* Syntatic identity will be denoted by {{M|\equiv}}, so {{M|M\equiv N}} will mean that {{M|M}} is exactly the same term as {{M|N}}
 +
===Length of a term===
 +
The length of a term {{M|M}} is denoted {{M|\text{lng}(M)}} and is the total number of occurrences of atoms in {{M|M}}
 +
===Occurs in===
 +
See page 6 of<ref name="LCAC"/>
 +
===Scope===
 +
(This is similar to scopes in programming languages)<br/>
 +
For a particular occurrence of {{M|\lambda x.M}} in a {{lambda|term}} {{M|P}}, the occurrence of {{M|M}} is called the ''scope'' of the occurrence of {{M|\lambda x}} immediately to the left.
  
 +
==Free and bound variables==
 +
An occurrence of a variable {{M|x}} in a term {{M|P}} is called:
 +
* ''Bound'' if it is in the scope of a {{M|\lambda x}} in {{M|P}}
 +
* ''Bound and binding'' if and only if it is the {{M|x}} in {{M|\lambda x}}
 +
* ''Free'' otherwise.
 +
In addition:
 +
* If {{M|x}} has at least one ''binding'' occurrence in {{M|P}} we call it a ''bound variable of {{M|P}}''
 +
** This requires thought but once it clicks it should be obvious, any variable that is a parameter of a function is a bound variable (at some point, even if unused)
 +
* If {{M|x}} has at least one ''free'' occurrence in {{M|P}} we call it a ''free variable of {{M|P}}''
 +
* We denote the set of free variables of {{M|P}} as: {{M|\text{FV}(P)}}
 +
 +
==Substitution==
 +
For any {{M|M}}, {{M|N}} and {{M|x}} define:
 +
* {{M|[N/x]M}} as the result of ''substituting'' {{M|N}} for every ''free'' occurrence of {{M|x}} in M, and changing the bound variables to avoid name clashes.
 +
The exact definition is given inductively as follows
 +
# {{M|[N/x]x \equiv N}}
 +
(more to come, there's 7 in total)
 
==Notes==
 
==Notes==
 
<references group="Note"/>
 
<references group="Note"/>

Revision as of 20:41, 11 August 2015

This is a NOTES page, so it isn't an actual page in the wiki yet!

Lambda terms

We define λ-terms as follows:[1]
Let the following be given:

  • Variables: an infinite sequence of expressions, v1,,vn [Note 1]
  • Atomic constants: a sequence of expressions again, that may also be finite or empty

The set of expressions called λ-terms is defined inductively as follows:

  1. All variables and atomic constants are λ-terms
    • These are known as atoms
  2. If M and N are λ-terms then (MN) is a λ-term
    • Known as applications
    • this is a short hand for M(N) in our modern terminology[1]
  3. If M is any λ-term and x any variable then (λx.M) is a λ-term
    • Any such expression is called an abstraction

Examples

  • (λv0.(v0v00)) - a function that xx(v00) I think

Here x, y and z are distinct variables:

  • (λx.(xy)) - a function that xx(y) I think
  • ((λy.y)(λx.(xy))) - This is difficult to put into words, but simply results in the function that xx(y)
  • (x(λx.(λx.x))) - This is nasty, it looks like x(x)
  • (λx.(yz)) 'constant' function that xy(z)

Notations

  • Capital letters denote arbitrary λ- terms
  • x,y,z,u,v,w will denote variables
  • Brackets will be skipped where it is understood that things are left associative, that is:
    • MNPQ is understood to mean (((MN)P)Q) (which to us means: ((M(N))(P))(Q) - you can see why this notation is dropped!)
  • (λx.(PQ)) will become λx.PQ
  • (λx1.(λx2.((λxn.M)))). becomes λx1x2xn.M
  • Syntatic identity will be denoted by , so MN will mean that M is exactly the same term as N

Length of a term

The length of a term M is denoted lng(M) and is the total number of occurrences of atoms in M

Occurs in

See page 6 of[1]

Scope

(This is similar to scopes in programming languages)
For a particular occurrence of λx.M in a λ-term P, the occurrence of M is called the scope of the occurrence of λx immediately to the left.

Free and bound variables

An occurrence of a variable x in a term P is called:

  • Bound if it is in the scope of a λx in P
  • Bound and binding if and only if it is the x in λx
  • Free otherwise.

In addition:

  • If x has at least one binding occurrence in P we call it a bound variable of P
    • This requires thought but once it clicks it should be obvious, any variable that is a parameter of a function is a bound variable (at some point, even if unused)
  • If x has at least one free occurrence in P we call it a free variable of P
  • We denote the set of free variables of P as: FV(P)

Substitution

For any M, N and x define:

  • [N/x]M as the result of substituting N for every free occurrence of x in M, and changing the bound variables to avoid name clashes.

The exact definition is given inductively as follows

  1. [N/x]xN

(more to come, there's 7 in total)

Notes

  1. Jump up The book uses v0,v00,v000, for some yet unknown reason

References

  1. Jump up to: 1.0 1.1 1.2 Lambda Calculus and Combinators, an introduction, J. Roger Hindley and Jonathan P. Seldin