In computer science, Scott encoding is a way to embed inductive datatypes in the lambda calculus, with somewhat different properties than (the similarly-motivated) Church encoding. Mogensen–Scott encoding extends and slightly modifies this to an embedding of all terms of the untyped lambda calculus.
The Scott encoding of constructor Ci of D is
Mogensen extends Scott encoding to all untyped lambda terms:
The idea here is to treat "lambda term" as a sum type with three cases: atom (constructor a, arity 1, not recursive), function application (constructor b, arity 2, recursive in both arguments), and lambda-abstraction (constructor c, arity 1, recursive). The only part of this encoding that does not follow immediately from that idea is how to deal with variables and binding of variables.
Comparison to the Church encoding
The Scott and Church encodings coincide on enumerated datatypes such as the boolean datatype.
Church encoded data and operations on them are typable in system F, but Scott encoded data and operations are not obviously typable in system F. Universal as well as recursive types appear to be required, and since strong normalization does not hold for recursively typed lambda calculus, termination of programs manipulating Scott-encoded data cannot be established by determining well-typedness of such programs.
- See the note "Types for the Scott numerals" by Martín Abadi, Luca Cardelli and Gordon Plotkin (February 18, 1993).
- Directly Reﬂective Meta-Programming
- Torben Mogensen (1992). Efficient Self-Interpretation in Lambda Calculus. Journal of Functional Programming.
|This computer science article is a stub. You can help Wikipedia by expanding it.|