- Mogensen-Scott encoding
In
computer science , Scott encoding is a way to embedinductive datatype s in thelambda calculus . Mogensen-Scott encoding extends and slightly modifies this to an embedding of all terms of the untyped lambda calculus.Definition
Let "D" be a datatype with "N" constructors, C_i}_{i=1}^N, such that constructor "Ci" has arity "Ai".
Church encoding
For comparison, the
Church encoding of constructor "Ci" of "D" is:lambda x_1 ldots x_{A_i} . lambda c_1 ldots c_N . c_i (x_1 c_1 ldots c_N) ldots (x_{A_i} c_1 ldots c_N)cott encoding
The Scott encoding of constructor "Ci" of "D" is:lambda x_1 ldots x_{A_i} . lambda c_1 ldots c_N . c_i x_1 ldots x_{A_i}
Mogensen-Scott encoding
Mogensen extends Scott encoding to all untyped lambda terms::egin{matrix} [x] & = & lambda a b c . a x \ [M N] & = & lambda a b c . b [M] [N] \ [lambda x . M] & = & lambda a b c . c lambda x . [M] \end{matrix}
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 sincestrong 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.References
* [http://cl.cse.wustl.edu/archon/archon.pdf Directly Reflective Meta-Programming]
Wikimedia Foundation. 2010.