Programming Language Theory

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

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 Combinatorial logic.

The integers (or any countably infinite set) can be represented via the Church encoding:

• 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. fⁿx
• plus ≡ λm. λn. λf. λx. m f (n f x) (from f^{(m + n)}(x) = f^m(fⁿ(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)} = (f^m)ⁿ)

The Church booleans take two arguments, and evaluate to one of them:

• true ≡ λa. λb . a
• false ≡ λa. λb . b

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