Programming Language Theory: Difference between revisions
No edit summary |
No edit summary |
||
| Line 6: | Line 6: | ||
===Untyped λ-calculus=== | ===Untyped λ-calculus=== | ||
Two operators (function ''definition'' and ''application'') upon one operand type (λ-expression). | Two operators (function ''definition'' and ''application'') upon one operand type (λ-expression). | ||
* Function definition: <tt>(λ''formalparam'' . body)</tt> | * Function definition: <tt>(λ''formalparam''. body)</tt> | ||
* Function application: <tt>function(''actualparam'')</tt> | * Function application: <tt>function(''actualparam'')</tt> | ||
The integers (or any countably infinite set) can be represented via the [http://en.wikipedia.org/wiki/Church_encoding Church encoding]: | The integers (or any countably infinite set) can be represented via the [http://en.wikipedia.org/wiki/Church_encoding Church encoding]: | ||
* <tt>n ≡ λf . λx . f<sup>n</sup>x</tt> | * <tt>n ≡ λf. λx . f<sup>n</sup>x</tt> | ||
* <tt>plus ≡ λm . λn . λf . λx . m f (n f x)</tt> (from f<sup>(m + n)</sup>(x) = f<sup>m</sup>(f<sup>n</sup>(x))) | * <tt>plus ≡ λm. λn. λf. λx. m f (n f x)</tt> (from f<sup>(m + n)</sup>(x) = f<sup>m</sup>(f<sup>n</sup>(x))) | ||
* <tt>succ ≡ λn.λf.λx. f (n f x)</tt> | |||
Common syntactic sugar: | Common syntactic sugar: | ||
* Left-associative application as implicit parentheses | * Left-associative application as implicit parentheses | ||
* Use of definitions (allowing identifiers to stand in as λ-expressions) | * Use of definitions (allowing identifiers to stand in as λ-expressions) | ||
* Currying: <tt>(λx, y . x + y)</tt> rather than <tt>(λx . (λy . x + y))</tt> | * Currying: <tt>(λx, y. x + y)</tt> rather than <tt>(λx. (λy. x + y))</tt> | ||
* Numeric literals rather than Church encoding | * Numeric literals rather than Church encoding | ||