Check out my first novel, midnight's simulacra!

Programming Language Theory: Difference between revisions

From dankwiki
No edit summary
Line 4: Line 4:
* Formal functional system (<tt>ffp</tt>): Extensible functional forms, functions represented by objects, translation of object representation to applicable form, formal semantics
* Formal functional system (<tt>ffp</tt>): Extensible functional forms, functions represented by objects, translation of object representation to applicable form, formal semantics
* Applicative state transition system (<tt>ast</tt>): <tt>ffp</tt> plus mutable state and coarse-grained operations thereupon
* Applicative state transition system (<tt>ast</tt>): <tt>ffp</tt> plus mutable state and coarse-grained operations thereupon
===Combinatory Logic===
===Untyped λ-calculus===
===Untyped λ-calculus===
Two operators (function ''definition'' and ''application'') upon one operand type (λ-expression).
Two operators (function ''definition'' and ''application'') upon one operand type (λ-expression).
* 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 [http://en.wikipedia.org/wiki/Combinatory_logic combinatory 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 [[Programming_Language_Theory#Combinatory_Logic|combinatory 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:12, 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

Combinatory Logic

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