en>LujViton: /* External links */ broken link replaced with new

2014-01-30T21:48:59Z

External links: broken link replaced with new

New page

In [[computer science]], '''Scott encoding''' is a way to represent [[Recursive data type|(recursive) data type]]s in the [[lambda calculus]]. [[Church encoding]] performs a similar function. The data and operators form a mathematical structure which is [[embedding|embedded]] in the lambda calculus.

Where as Church encoding starts with representations of the basic data types, and builds up from it, Scott encoding starts from the simplest method to compose [[algebraic data types]].

'''Mogensen–Scott encoding''' extends and slightly modifies Scott encoding by applying the encoding to [[Metaprogramming]]. This encoding allows the representation of [[untyped lambda calculus|lambda calculus]] terms, as data, to be operated on by a meta program.

==History==

Scott encoding appears first in a set of unpublished lecture notes by [[Dana Scott]]. [[Torben Mogensen]] later extended Scott encoding for the encoding of Lambda terms as data. <ref>
{{ cite journal|
last=Mogensen|
first=Torben|
title=Efficient Self-Interpretation in Lambda Calculus|
journal=Journal of Functional Programming|
year=1994|
volume=2|
pages=345-364}}
</ref>

==Discussion==

Lambda calculus allows data to be stored as [[Parameter (computer programming)|parameters]] to a function that does not yet have all the parameters required for application. For example,

: <math> ((\lambda x_1 \ldots x_n.\lambda c.c\ x_1 \ldots x_n)\ v_1 \ldots v_n)\ f </math>

May be thought of as a record or struct where the fields <math> x_1 \ldots x_n </math> have been initialized with the values <math> v_1 \ldots v_n </math>. These values may then be accessed by applying the term to a function ''f''. This reduces to,

: <math> f\ v_1 \ldots v_n </math>

''c'' may represent a constructor for an algebraic data type in functional languages such as [[Haskell (programming language)|Haskell]]. Now suppose there ''N'' constructors, each with <math>A_i</math> arguments;
{| class="wikitable"
|-
! Constructor !! Given arguments !! Result
|-
| <math> ((\lambda x_1 \ldots x_{A_1}.\lambda c_1 \ldots c_N.c_1\ x_1 \ldots x_{A_1})\ v_1 \ldots v_{A_1}) </math>
| <math> f_1 \ldots f_N </math>
| <math> f_1\ v_1 \ldots v_{A_1} </math>
|-
| <math> ((\lambda x_1 \ldots x_{A_1}.\lambda c_1 \ldots c_N.c_2\ x_1 \ldots x_{A_2})\ v_1 \ldots v_{A_2}) </math>
| <math> f_1 \ldots f_N </math>
| <math> f_2\ v_1 \ldots v_{A_2} </math>
|-
| colspan='3' align='center' style='border-left: 1px solid white; border-right: 1px solid white' | ...
|-
| <math> ((\lambda x_1 \ldots x_{A_N}.\lambda c_1 \ldots c_N.c_N\ x_1 \ldots x_{A_N})\ v_1 \ldots v_{A_N}) </math>
| <math> f_1 \ldots f_N </math>
| <math> f_N\ v_1 \ldots v_{A_1} </math>
|}

Each constructor selects a different function from the function parameters <math> f_1 \ldots f_N </math>. This provides branching in the process flow, based on the constructor. Each constructor may have a different [[arity]] (number of parameters). If the constructors have no parameters then the set of constructors acts like an ''enum''; a type with a fixed number of values. If the constructors have parameters, recursive data structures may be constructed.

==Definition==
Let ''D'' be a datatype with ''N'' [[Algebraic data type|constructors]], <math>\{c_i\}_{i=1}^N</math>, such that constructor <math>c_i</math> has [[arity]] <math>A_i</math>.

===Scott encoding===

The Scott encoding of constructor <math>c_i</math> of the data type ''D'' is
: <math>\lambda x_1 \ldots x_{A_i} . \lambda c_1 \ldots c_N . c_i\ x_1 \ldots x_{A_i}</math>

=== Mogensen–Scott encoding===

Mogensen extends Scott encoding to encode any untyped lambda term as data. This allows a lambda term to be represented as data, within a Lambda calculus [[Metaprogramming|meta program]]. The meta function ''mse'' converts a lambda term into the corresponding data representation of the lambda term;
:<math>\begin{array}{rcl}
\operatorname{mse}[x] & = & \lambda a, b, c.a\ x \\
\ \operatorname{mse}[M\ N] & = & \lambda a, b, c.b\ \operatorname{mse}[M]\ \operatorname{mse}[N] \\
\ \operatorname{mse}[\lambda x . M] & = & \lambda a, b, c.c\ (\lambda x.\operatorname{mse}[M]) \\
\end{array}</math>

The "lambda term" is represented as a [[tagged union]] with three cases:
* Constructor ''a'' - a variable ([[Arity|arity]] 1, not recursive)
* Constructor ''b'' - function application (arity 2, recursive in both arguments),
* Constructor ''c'' - lambda-abstraction (arity 1, recursive).

For example,

: <math> \operatorname{mse}[\lambda x.f\ (x\ x)]</math>
: <math> \lambda a, b, c.c\ (\lambda x.\operatorname{mse}[f\ (x\ x)])</math>
: <math> \lambda a, b, c.c\ (\lambda x.\lambda a, b, c.b\ \operatorname{mse}[f]\ \operatorname{mse}[x\ x])</math>
: <math> \lambda a, b, c.c\ (\lambda x.\lambda a, b, c.b\ (\lambda a, b, c.a\ f)\ \operatorname{mse}[x\ x])</math>
: <math> \lambda a, b, c.c\ (\lambda x.\lambda a, b, c.b\ (\lambda a, b, c.a\ f)\ (\lambda a, b, c.b\ \operatorname{mse}[x]\ \operatorname{mse}[x]))</math>
: <math> \lambda a, b, c.c\ (\lambda x.\lambda a, b, c.b\ (\lambda a, b, c.a\ f)\ (\lambda a, b, c.b\ (\lambda a, b, c.a\ x)\ (\lambda a, b, c.a\ x)))</math>

==Comparison to the Church encoding==

The Scott encoding coincides with the [[Church encoding]] for booleans. Church encoding of pairs may be generalized to arbitrary data types by encoding <math>c_i</math> of ''D'' above as

: <math>\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)</math>
compare this to the Mogensen Scott encoding,
: <math>\lambda x_1 \ldots x_{A_i} . \lambda c_1 \ldots c_N . c_i x_1 \ldots x_{A_i}</math>

With this generalization, the Scott and Church encodings coincide on all enumerated datatypes (such as the boolean datatype) because each constructor is a constant (no parameters).

==Type definitions==

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,<ref>See the note [http://lucacardelli.name/Papers/Notes/scott2.pdf "Types for the Scott numerals"] by Martín Abadi, Luca Cardelli and Gordon Plotkin (February 18, 1993).</ref> 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 also==

* [[Church encoding]]
* [[System F]]
* [[Lambda cube]]

==Notes==

{{Reflist}}

==References==
*[http://www.divms.uiowa.edu/~astump/papers/archon.pdf Directly Reﬂective Meta-Programming]
*Torben Mogensen (1992). [ftp://ftp.diku.dk/diku/semantics/papers/D-128.ps.Z Efficient Self-Interpretation in Lambda Calculus]. '' Journal of Functional Programming''.

{{DEFAULTSORT:Mogensen-Scott encoding}}
[[Category:Lambda calculus]]

{{compsci-stub}}

Wind - Revision history

en>LujViton: /* External links */ broken link replaced with new