Check out my first novel, midnight's simulacra!

Programming Language Theory: Difference between revisions

From dankwiki
No edit summary
Line 8: Line 8:
* Function definition: <tt>(λ''boundparam''. body)</tt>
* Function definition: <tt>(λ''boundparam''. body)</tt>
* Function application: <tt>function(''actualparam'')</tt>
* Function application: <tt>function(''actualparam'')</tt>
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 [[Architecture|Combinatorial logic]].
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 [[Architecture|combinatorial logic]].


The integers (or any countably infinite set) can be represented via the [http://en.wikipedia.org/wiki/Church_encoding Church encoding] (or [http://en.wikipedia.org/wiki/Mogensen-Scott_encoding Mogensen-Scott], or others):
The integers (or any countably infinite set) can be represented via the [http://en.wikipedia.org/wiki/Church_encoding Church encoding] (or [http://en.wikipedia.org/wiki/Mogensen-Scott_encoding Mogensen-Scott], or others):

Revision as of 06:05, 7 December 2009

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 (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
  • 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)

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