In
computer science
Computer science is the study of computation, automation, and information. Computer science spans theoretical disciplines (such as algorithms, theory of computation, information theory, and automation) to Applied science, practical discipli ...
, Scott encoding is a way to represent
(recursive) data types in the
lambda calculus
Lambda calculus (also written as ''λ''-calculus) is a formal system in mathematical logic for expressing computation based on function abstraction and application using variable binding and substitution. It is a universal model of computation ...
.
Church encoding
In mathematics, Church encoding is a means of representing data and operators in the lambda calculus. The Church numerals are a representation of the natural numbers using lambda notation. The method is named for Alonzo Church, who first encoded da ...
performs a similar function. The data and operators form a mathematical structure which is
embedded in the lambda calculus.
Whereas 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
In computer programming, especially functional programming and type theory, an algebraic data type (ADT) is a kind of composite type, i.e., a type formed by combining other types.
Two common classes of algebraic types are product types (i.e., t ...
.
Mogensen–Scott encoding extends and slightly modifies Scott encoding by applying the encoding to
Metaprogramming
Metaprogramming is a programming technique in which computer programs have the ability to treat other programs as their data. It means that a program can be designed to read, generate, analyze or transform other programs, and even modify itself ...
. This encoding allows the representation of
lambda calculus
Lambda calculus (also written as ''λ''-calculus) is a formal system in mathematical logic for expressing computation based on function abstraction and application using variable binding and substitution. It is a universal model of computation ...
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
Dana Stewart Scott (born October 11, 1932) is an American logician who is the emeritus Hillman University Professor of Computer Science, Philosophy, and Mathematical Logic at Carnegie Mellon University; he is now retired and lives in Berkeley, Ca ...
whose first citation occurs in the book ''Combinatorial Logic, Volume II''.
Michel Parigot
Michel may refer to:
* Michel (name), a given name or surname of French origin (and list of people with the name)
* Míchel (nickname), a nickname (a list of people with the nickname, mainly Spanish footballers)
* Míchel (footballer, born 1963), S ...
gave a logical interpretation of and strongly
normalizing recursor for Scott-encoded numerals, referring to them as the "Stack type" representation of numbers.
Torben Mogensen Torben is a Danish variant of the given name Torbjörn.
People named Torben include:
*Torben Betts (born 1968), English playwright and screenwriter
*Torben Boye (born 1966), Danish former footballer
*Torben Frank (born 1968), Danish former footbal ...
later extended Scott encoding for the encoding of Lambda terms as data.
Discussion
Lambda calculus allows data to be stored as
parameters
A parameter (), generally, is any characteristic that can help in defining or classifying a particular system (meaning an event, project, object, situation, etc.). That is, a parameter is an element of a system that is useful, or critical, when ...
to a function that does not yet have all the parameters required for application. For example,
:
May be thought of as a record or struct where the fields
have been initialized with the values
. These values may then be accessed by applying the term to a function ''f''. This reduces to,
:
''c'' may represent a constructor for an algebraic data type in functional languages such as
Haskell
Haskell () is a general-purpose, statically-typed, purely functional programming language with type inference and lazy evaluation. Designed for teaching, research and industrial applications, Haskell has pioneered a number of programming lang ...
. Now suppose there are ''N'' constructors, each with
arguments;
:
Each constructor selects a different function from the function parameters
. This provides branching in the process flow, based on the constructor. Each constructor may have a different
arity
Arity () is the number of arguments or operands taken by a function, operation or relation in logic, mathematics, and computer science. In mathematics, arity may also be named ''rank'', but this word can have many other meanings in mathematics. In ...
(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''
constructors,
, such that constructor
has
arity
Arity () is the number of arguments or operands taken by a function, operation or relation in logic, mathematics, and computer science. In mathematics, arity may also be named ''rank'', but this word can have many other meanings in mathematics. In ...
.
Scott encoding
The Scott encoding of constructor
of the data type ''D'' is
:
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
meta program. The meta function ''mse'' converts a lambda term into the corresponding data representation of the lambda term;
:
The "lambda term" is represented as a
tagged union
In computer science, a tagged union, also called a variant, variant record, choice type, discriminated union, disjoint union, sum type or coproduct, is a data structure used to hold a value that could take on several different, but fixed, types. O ...
with three cases:
* Constructor ''a'' - a variable (
arity
Arity () is the number of arguments or operands taken by a function, operation or relation in logic, mathematics, and computer science. In mathematics, arity may also be named ''rank'', but this word can have many other meanings in mathematics. In ...
1, not recursive)
* Constructor ''b'' - function application (arity 2, recursive in both arguments),
* Constructor ''c'' - lambda-abstraction (arity 1, recursive).
For example,
:
Comparison to the Church encoding
The Scott encoding coincides with the
Church encoding
In mathematics, Church encoding is a means of representing data and operators in the lambda calculus. The Church numerals are a representation of the natural numbers using lambda notation. The method is named for Alonzo Church, who first encoded da ...
for booleans. Church encoding of pairs may be generalized to arbitrary data types by encoding
of ''D'' above as
:
compare this to the Mogensen Scott encoding,
:
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).
Concerning the practicality of using either the Church or Scott encoding for programming, there is a symmetric trade-off: Church-encoded numerals support a constant-time addition operation and have no better than a linear-time predecessor operation; Scott-encoded numerals support a constant-time predecessor operation and have no better than a linear-time addition operation.
Type definitions
Church-encoded data and operations on them are typable in
system F
System F (also polymorphic lambda calculus or second-order lambda calculus) is a typed lambda calculus that introduces, to simply typed lambda calculus, a mechanism of universal quantification over types. System F formalizes parametric polymorphis ...
, as are Scott-encoded data and operations. However, the encoding is significantly more complicated.
The type of the Scott encoding of the natural numbers is the positive recursive type:
:
Full recursive types are not part of System F, but positive recursive types can are expressible in System F via the encoding:
:
Combining these twos fact yields the System F type of the Scott encoding:
:
This can be contrasted with the type of the Church encoding:
:
The Church encoding is a second-order type, but the Scott encoding is fourth-order!
See also
*
Church encoding
In mathematics, Church encoding is a means of representing data and operators in the lambda calculus. The Church numerals are a representation of the natural numbers using lambda notation. The method is named for Alonzo Church, who first encoded da ...
*
System F
System F (also polymorphic lambda calculus or second-order lambda calculus) is a typed lambda calculus that introduces, to simply typed lambda calculus, a mechanism of universal quantification over types. System F formalizes parametric polymorphis ...
*
Lambda cube
In mathematical logic and type theory, the λ-cube (also written lambda cube) is a framework introduced by Henk Barendregt to investigate the different dimensions in which the calculus of constructions is a generalization of the simply typed λ- ...
Notes
References
*Stump, A. (2009)
Directly reflective meta-programming ''Higher-Order and Symbolic Computation, 22'', 115-144.
*Mogensen, T.Æ. (1992)
Efficient Self-Interpretations in lambda Calculus ''J. Funct. Program., 2'', 345-363.
{{DEFAULTSORT:Mogensen-Scott encoding
Lambda calculus