# Encoding schemes in lambda calculi

## Nothing but functions

In the context of lambda calculi, an _encoding_ is a way of representing a particular programming language construct.

An _encoding scheme_ is a comprehensive set of definitions that consistently represents a functional subset of a common programming language entities. It's a set of definitions that makes lambda calculus a working programming language (despite being minimal and horribly uncomfortable).

A purpose of encoding, and encoding schemes especially, is to demonstrate that it is possible to create a fully functional (even Turing complete) programming language despite such a barren environment, that offers only anonymous functions. All you need are anonymous functions, that is all you need.

An encoding scheme includes primitives such as Booleans, logical ops and connectives, natural numbers, arithmetic ops, and so on. This layer can then support additional language elements such as different data structures: pair, tuple, list, tree, as well as operations that manipulate them.

Naturally, the author of the lambda calculus, Alonzo Church, has invented the most comprehensive set of definitions of how to encode many mathematical objects including Booleans, natural numbers, predicates, negative, rational, real numbers, and various data structures. Such an encoding scheme (set of encodings) has come to be known as the _the Church encoding_.

Besides inventing the lambda calculus, Alonzo Church was the first to come up with own comprehensive set of encodings, called the _Church encoding_. It is a collection of concrete lambda expressions used to represent many PL concepts including Booleans, logical connectives, predicates, natural numbers, data structures, related operations. In fact, many of the constituent concepts of the Church encoding bear Church's name as well: Church Booleans, Church numerals, Church pair, Church list, etc.

_Church Booleans_ is the name for concrete functions (lambda abstractions) that Church created in order to represent the truth values (true and false), as well as the logical connectives (and, or, not, etc.), predicates and conditionals (i.e. functions that return a truth value (isTrue, isTautology, isMonotonic), and related operations (createTruthTable, meet, findJoin).

_Church numerals_ are representations of the natural numbers using lambda terms.

## Overview of encoding schemes in lambda calculi

## Lambda calculi encoding schemes

* Church encoding
* Scott encoding
* Mogensen-Scott encoding
* Böhm-Berarducci encoding
* Parigot encoding

## Encoding schemes

_Scott encoding_ is a way to represent potentially recursive data types in the lambda calculus.

Scott encoding uses the idea of continuations and can lead to simpler code.

Scott encoding can be done in untyped lambda calculus, whereas its use with types requires a type system with recursion and type polymorphism.

The data and operators form a mathematical structure which is embedded in the lambda calculus.

_Church encoding_ performs a similar function, but 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_.

_Mogensen-Scott encoding_ extends and slightly modifies Scott encoding by applying the encoding to metaprogramming. This encoding allows the representation of lambda calculus terms, as data, to be operated on by a meta program.

Scott encoding appears first in a set of unpublished lecture notes by Dana Scott whose first citation occurs in the book "Combinatorial Logic, Volume II".

_Michel Parigot_ 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_ later extended Scott encoding for the encoding of Lambda terms as data.
