Programming Language Theory

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.

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).

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. fⁿx

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) = 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)ⁿ)

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