Check out my first novel, midnight's simulacra!

Programming Language Theory

From dankwiki
Revision as of 08:15, 7 December 2009 by Dank (talk | contribs) (→‎Evaluation)

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.

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. Application of the a rule preserves its equivalence.:

  • ɑ-conversion renames bound variables with any variable y which is not free, preserving ɑ-equivalence:
    • λx. m →ɑ λy. {y / x}m
  • β-reduction replaces a formal parameter with an actual parameter, preserving β-equivalence:
    • (λx. m) n →β {n / x}m
    • An expression is in β-normal form if no β-reductions are possible. It is otherwise a β-redex.
  • η-reduction eliminates bindings unused within a scope, preserving η-equivalence:
    • (λx. (f x)) →η f
    • An expression is in β-η-normal form ("Beta-eta-normal form") if neither β- nor η-reductions are possible
      • If a η-reduction is applicable, the expression is a η-redex.

According to the Church-Rosser Theorem, all terminating evaluations will compute the same function. Certain application orders might not terminate for a given expression, though, despite termination via other orders. This gives rise to the core difference between call-by-value and call-by-name semantics:

  • leftmost-innermost application evaluates arguments as soon as possible, and is equivalent to leftmost call-by-value ("applicative order")
  • leftmost-outermost application substitutes prior to evaluation, and is equivalent to lazy call-by-name (call-by-necessity, "normal order")

Call-by-name terminates if any order does, but might require more total reductions. Call-by-value only β-reduces abstractions, not applications. Call-by-need memoizes the results of evaluated functions, and is equivalent to call-by-name if side-effects are disallowed. Call-by-name is text substitution augmented by capture avoidance.

Numerics

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

Some basic arithmetic 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 our 1 from above)
  • mult ≡ λm. λn. λf. n (m f) (from f(m * n) = (fm)n)
  • pow ≡ λm. λn. n m
  • pred ≡ λn. λf. λx. n (λg. λh. h (g f)) (λu. x) (λu. u) (returns 0 when applied to 0)
  • sub ≡ λm. λn. (n pred) m (using pred from above)

Logic

The Church booleans evaluate to one of their two arguments:

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

Using them, we implement basic conditional logic:

  • if[A, B, C] ≡ A B C (use true/false for A. Evaluates to B on true, C on false)
  • not ≡ λt. t false true (β-equivalent to if[A, false, true])

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