Difference between revisions of "Notes:Lambda calculus"
From Maths
(Saving progress so far) |
m (→Substitution: Finished substitution section) |
||
| (One intermediate revision by the same user not shown) | |||
| 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}} | ||
| + | # {{M|[N/x]a \equiv a}} for all ''atoms'' {{M|a\not\equiv x}} | ||
| + | # {{M|[N/x](PQ)\equiv ([N/x]P[N/x]Q)}} | ||
| + | # {{M|[N/x](\lambda x.P)\equiv \lambda x.P}} | ||
| + | #* This demonstrates scoping well, even if {{M|x}} occurs in {{M|P}} it's bound already, and not free. | ||
| + | # {{M|[N/x](\lambda y.P)\equiv \lambda y.P}} if {{M|x\not\in\text{FV}(P)}} | ||
| + | # {{M|[N/x](\lambda y.P)\equiv \lambda y.[N/x]P}} if {{M|x\in\text{FV}(P)}} and {{M|y\not\in\text{FV}(N)}} | ||
| + | # {{M|[N/x](\lambda y.P)\equiv \lambda z.[N/x][z/y]P}} if {{M|x\in\text{FV}(P)}} and {{M|x\in\text{FV}(N)}} where {{M|z}} is the first variable {{M|\not\in\text{FV}(NP)}} | ||
| + | Note: | ||
| + | * For the last 3 we assume that {{M|x\not\equiv y}} | ||
==Notes== | ==Notes== | ||
Latest revision as of 21:22, 11 August 2015
This is a NOTES page, so it isn't an actual page in the wiki yet!
Contents
Lambda terms
We define [ilmath]\lambda[/ilmath]-terms as follows:[1]
Let the following be given:
- Variables: an infinite sequence of expressions, [ilmath]v_1,\ldots,v_n\ldots[/ilmath] [Note 1]
- Atomic constants: a sequence of expressions again, that may also be finite or empty
The set of expressions called [ilmath]\lambda[/ilmath]-terms is defined inductively as follows:
- All variables and atomic constants are [ilmath]\lambda[/ilmath]-terms
- These are known as atoms
- If [ilmath]M[/ilmath] and [ilmath]N[/ilmath] are [ilmath]\lambda[/ilmath]-terms then [ilmath](MN)[/ilmath] is a [ilmath]\lambda[/ilmath]-term
- Known as applications
- this is a short hand for [ilmath]M(N)[/ilmath] in our modern terminology[1]
- If [ilmath]M[/ilmath] is any [ilmath]\lambda[/ilmath]-term and [ilmath]x[/ilmath] any variable then [ilmath](\lambda x.M)[/ilmath] is a [ilmath]\lambda[/ilmath]-term
- Any such expression is called an abstraction
Examples
- [ilmath](\lambda v_0.(v_0v_{00}))[/ilmath] - a function that [ilmath]x\mapsto x(v_{00})[/ilmath] I think
Here [ilmath]x[/ilmath], [ilmath]y[/ilmath] and [ilmath]z[/ilmath] are distinct variables:
- [ilmath](\lambda x.(xy))[/ilmath] - a function that [ilmath]x\mapsto x(y)[/ilmath] I think
- [ilmath]((\lambda y.y)(\lambda x.(xy)))[/ilmath] - This is difficult to put into words, but simply results in the function that [ilmath]x\mapsto x(y)[/ilmath]
- [ilmath](x(\lambda x.(\lambda x.x)))[/ilmath] - This is nasty, it looks like [ilmath]x(x)[/ilmath]
- [ilmath](\lambda x.(yz))[/ilmath] 'constant' function that [ilmath]x\mapsto y(z)[/ilmath]
Notations
- Capital letters denote arbitrary [ilmath]\lambda[/ilmath]- terms
- [ilmath]x,y,z,u,v,w[/ilmath] will denote variables
- Brackets will be skipped where it is understood that things are left associative, that is:
- [ilmath]MNPQ[/ilmath] is understood to mean [ilmath](((MN)P)Q)[/ilmath] (which to us means: [ilmath]((M(N))(P))(Q)[/ilmath] - you can see why this notation is dropped!)
- [ilmath](\lambda x.(PQ))[/ilmath] will become [ilmath]\lambda x.PQ[/ilmath]
- [ilmath](\lambda x_1.(\lambda x_2.(\ldots(\lambda x_n.M)\ldots))).[/ilmath] becomes [ilmath]\lambda x_1x_2\ldots x_n.M[/ilmath]
- Syntatic identity will be denoted by [ilmath]\equiv[/ilmath], so [ilmath]M\equiv N[/ilmath] will mean that [ilmath]M[/ilmath] is exactly the same term as [ilmath]N[/ilmath]
Length of a term
The length of a term [ilmath]M[/ilmath] is denoted [ilmath]\text{lng}(M)[/ilmath] and is the total number of occurrences of atoms in [ilmath]M[/ilmath]
Occurs in
See page 6 of[1]
Scope
(This is similar to scopes in programming languages)
For a particular occurrence of [ilmath]\lambda x.M[/ilmath] in a [ilmath]\lambda[/ilmath]-term [ilmath]P[/ilmath], the occurrence of [ilmath]M[/ilmath] is called the scope of the occurrence of [ilmath]\lambda x[/ilmath] immediately to the left.
Free and bound variables
An occurrence of a variable [ilmath]x[/ilmath] in a term [ilmath]P[/ilmath] is called:
- Bound if it is in the scope of a [ilmath]\lambda x[/ilmath] in [ilmath]P[/ilmath]
- Bound and binding if and only if it is the [ilmath]x[/ilmath] in [ilmath]\lambda x[/ilmath]
- Free otherwise.
In addition:
- If [ilmath]x[/ilmath] has at least one binding occurrence in [ilmath]P[/ilmath] we call it a bound variable of [ilmath]P[/ilmath]
- 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 [ilmath]x[/ilmath] has at least one free occurrence in [ilmath]P[/ilmath] we call it a free variable of [ilmath]P[/ilmath]
- We denote the set of free variables of [ilmath]P[/ilmath] as: [ilmath]\text{FV}(P)[/ilmath]
Substitution
For any [ilmath]M[/ilmath], [ilmath]N[/ilmath] and [ilmath]x[/ilmath] define:
- [ilmath][N/x]M[/ilmath] as the result of substituting [ilmath]N[/ilmath] for every free occurrence of [ilmath]x[/ilmath] in M, and changing the bound variables to avoid name clashes.
The exact definition is given inductively as follows
- [ilmath][N/x]x \equiv N[/ilmath]
- [ilmath][N/x]a \equiv a[/ilmath] for all atoms [ilmath]a\not\equiv x[/ilmath]
- [ilmath][N/x](PQ)\equiv ([N/x]P[N/x]Q)[/ilmath]
- [ilmath][N/x](\lambda x.P)\equiv \lambda x.P[/ilmath]
- This demonstrates scoping well, even if [ilmath]x[/ilmath] occurs in [ilmath]P[/ilmath] it's bound already, and not free.
- [ilmath][N/x](\lambda y.P)\equiv \lambda y.P[/ilmath] if [ilmath]x\not\in\text{FV}(P)[/ilmath]
- [ilmath][N/x](\lambda y.P)\equiv \lambda y.[N/x]P[/ilmath] if [ilmath]x\in\text{FV}(P)[/ilmath] and [ilmath]y\not\in\text{FV}(N)[/ilmath]
- [ilmath][N/x](\lambda y.P)\equiv \lambda z.[N/x][z/y]P[/ilmath] if [ilmath]x\in\text{FV}(P)[/ilmath] and [ilmath]x\in\text{FV}(N)[/ilmath] where [ilmath]z[/ilmath] is the first variable [ilmath]\not\in\text{FV}(NP)[/ilmath]
Note:
- For the last 3 we assume that [ilmath]x\not\equiv y[/ilmath]
Notes
- ↑ The book uses [ilmath]v_0,v_{00},v_{000},\cdots[/ilmath] for some yet unknown reason
