Check out my first novel, midnight's simulacra!
Programming Language Theory: Difference between revisions
No edit summary |
|||
| Line 35: | Line 35: | ||
λ-abst ::= '(' 'λ'var'.' λ-term ')'</pre> | λ-abst ::= '(' 'λ'var'.' λ-term ')'</pre> | ||
====Evaluation==== | ====Evaluation==== | ||
We'll use a substitution syntax to rewrite λ-calculus strings. ''{N / X}M'' substitutes expression N for free instances of X in expression M: | |||
* If M is a variable ({N / X}V), replace M with X if and only if M is N. | |||
* If M is a λ-app ({N / X}(A B)), {N / X}M = (({N / X}A) ({N / X}B)) | |||
* Otherwise, M is a λ-abst ({N / X}(λV. B)). | |||
** If X is V, M is unchanged (X is bound in M). | |||
** If X does not appear in B, M is unchanged (no free X in M) | |||
** If V occurs free in N, substitute N for X throughout B. | |||
** Otherwise, the substitution in this form is invalid (but it can be made valid...) | |||
With this syntax, we define evaluation rules: | |||
* ''ɑ-conversion'': λX. M →<sub>ɑ</sub> λY. {Y / X}M. Renames bound variables with any variable Y which is not free in M. | * ''ɑ-conversion'': λX. M →<sub>ɑ</sub> λY. {Y / X}M. Renames bound variables with any variable Y which is not free in M. | ||
* ''β-reduction'': (λX. M) N →<sub>β</sub> {N / X}M. Replaces a formal parameter with an actual parameter. | * ''β-reduction'': (λX. M) N →<sub>β</sub> {N / X}M. Replaces a formal parameter with an actual parameter. | ||
Revision as of 07:27, 7 December 2009
The Church-Turing thesis equates a vaguely-defined set of "computable" functions with the partial recursive functions. Several systems are only as powerful as the partial recursives (Turing-complete): Turing machines and the λ-calculus are two. Programming languages provide further syntaxes and semantics, but all you really need in life is combinatory logic.
Applicative/Functional Programming
Expressions compose functions rather than values. Backus proposed three tiers of complexity in his Turing Award lecture:
- Simply functional language (fp): No state, limited names, finitely many functional forms, simple substitution semantics, algebraic laws
- Formal functional system (ffp): Extensible functional forms, functions represented by objects, translation of object representation to applicable form, formal semantics
- Applicative state transition system (ast): ffp plus mutable state and coarse-grained operations thereupon
Higher-order functions map one or more functions to a function.
Combinatory Logic
SKI Calculus
- I ≡ λx. x
- K ≡ λx, y. x
- S ≡ λx, y, z. (x z (y z))
Fixed-Point Combinators
Higher-order functions which compute the fixed points of their inputs. Curry's Y-combinator was the first:
- Y ≡ λf. (λx. f (x x)) (λx. f (x x)) (untyped λ-calculus)
- Y ≡ S (K (S I I)) (S (S (K S) K) (K (S I I))) (SKI calculus)
Divergence-free evaluation of the Y-combinator requires call-by-name semantics. Call-by-value semantics can make use of the Θv (Turing) or Z-combinators:
- Θv ≡ (λx. λy. (y (λz. x x y z))) (λx. λy. (y (λz. x x y z)))
- Z ≡ λf. (λx. f (λy. x x y)) (λx. f (λy. x x y)) (via η-expansion on Y)
The infinitely many fixed-point combinators of untyped λ-calculus are recursively enumerable.
Untyped λ-calculus
Two operators (function definition and application) upon one operand type (λ-expression).
- Function definition: (λboundparam. body)
- Function application: function(actualparam)
The body is made up of free and bound variables. Those not present in the λ's list of bound variables are free. A λ-expression with no free variables is closed (closed expressions are equivalent in power to combinatory logic). A λ-expression enclosed in scopes of its free variables is meaningful. Changing the names of bound variables within a λ-expression preserves ɑ-equivalence.
Grammar
λ-term ::= λ-app | λ-abst | var λ-app ::= λ-term λ-term λ-abst ::= 'λ'var'.' λ-term
This abstract grammar can be augmented with associativity rules and grouping syntax (parentheses) to provide a concrete grammar. If verbosity is no issue, no associativity rules need be specified for the following grammar:
λ-term ::= λ-app | λ-abst | var
λ-app ::= '(' λ-term λ-term ')'
λ-abst ::= '(' 'λ'var'.' λ-term ')'
Evaluation
We'll use a substitution syntax to rewrite λ-calculus strings. {N / X}M substitutes expression N for free instances of X in expression M:
- If M is a variable ({N / X}V), replace M with X if and only if M is N.
- If M is a λ-app ({N / X}(A B)), {N / X}M = (({N / X}A) ({N / X}B))
- Otherwise, M is a λ-abst ({N / X}(λV. B)).
- If X is V, M is unchanged (X is bound in M).
- If X does not appear in B, M is unchanged (no free X in M)
- If V occurs free in N, substitute N for X throughout B.
- Otherwise, the substitution in this form is invalid (but it can be made valid...)
With this syntax, we define evaluation rules:
- ɑ-conversion: λX. M →ɑ λY. {Y / X}M. Renames bound variables with any variable Y which is not free in M.
- β-reduction: (λX. M) N →β {N / X}M. Replaces a formal parameter with an actual parameter.
Encodings
The integers (or any countably infinite set) can be represented via the Church encoding (or Mogensen-Scott, or others):
- 0 ≡ λf. λx. x
- 1 ≡ λf. λx. f x
- 2 ≡ λf. λx. f (f x)
- 3 ≡ λf. λx. f (f (f x))
- n ≡ λf. λx. fnx
The Church booleans take two arguments, and evaluate to one of them:
- true ≡ λa. λb . a
- false ≡ λa. λb . b
Some basic operations:
- plus ≡ λm. λn. λf. λx. m f (n f x) (from f(m + n)(x) = fm(fn(x)))
- succ ≡ λn. λf. λx. f (n f x) (β-equivalent to (plus 1) for a defined 1)
- mult ≡ λm. λn. λf. n (m f) (from f(m * n) = (fm)n)
Common syntactic sugar:
- Left-associative application as implicit parentheses
- Use of definitions (allowing identifiers to stand in as λ-expressions)
- Currying: (λx, y. x + y) rather than (λx. (λy. x + y))
- Numeric literals rather than Church encoding
