Difference between revisions of "Notes:Lambda calculus"
From Maths
(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,\ | + | * ''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!
Contents
[hide]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:
- All variables and atomic constants are λ-terms
- These are known as atoms
- 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]
- 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 x↦x(v00) I think
Here x, y and z are distinct variables:
- (λx.(xy)) - a function that x↦x(y) I think
- ((λy.y)(λx.(xy))) - This is difficult to put into words, but simply results in the function that x↦x(y)
- (x(λx.(λx.x))) - This is nasty, it looks like x(x)
- (λx.(yz)) 'constant' function that x↦y(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 λx1x2…xn.M
- Syntatic identity will be denoted by ≡, so M≡N 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
- [N/x]x≡N
(more to come, there's 7 in total)
Notes
- Jump up ↑ The book uses v0,v00,v000,⋯ for some yet unknown reason
References
- ↑ Jump up to: 1.0 1.1 1.2 Lambda Calculus and Combinators, an introduction, J. Roger Hindley and Jonathan P. Seldin