In computer science, Scott encoding is a way to represent algebraic data types in the lambda calculus, following their syntactic definition without regard whether they are recursive or not. This is unlike Church encoding which treats recursive data types specially, representing them with right folds. The data and operators form a mathematical structure which is embedded in the lambda calculus. 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.
Exposition
Numbers Scott encoding of numbers follows the Peano definition of natural numbers as a sum of two cases, the zero case and the successor case,
N a t := Zero | Succ N a t {\displaystyle \qquad Nat:=\operatorname {Zero} \ |\,\operatorname {Succ} Nat}
Correspondingly, Scott numerals are functions which expect two arguments, two handlers, each receiving the corresponding case's data from the number:
0 = λ z s . z Succ = λ n . λ z s . s n {\displaystyle \quad {\begin{aligned}0&=\lambda zs.z\\\operatorname {Succ} &=\lambda n.\lambda zs.s\ n\end{aligned}}}
The zero case has no data. The successor case data is its Scott numeral, which is served as the argument to the corresponding handler. When a Scott numeral is supplied with two handlers, it calls the appropriate one with its corresponding data. Scott encoded values embody a choice between the sum data type's cases.
IsZero = λ n . n True ( λ m . False ) Pred = λ n . n 0 ( λ m . m ) {\displaystyle \quad {\begin{aligned}\operatorname {IsZero} &=\lambda n.n\ \operatorname {True} \ (\lambda m.\operatorname {False} )\\\operatorname {Pred} &=\lambda n.n\ 0\ (\lambda m.m)\end{aligned}}}
Recursive operations on Scott numerals require explicit use of recursion, e.g. using Y {\displaystyle \operatorname {Y} } combinator:
Add = Y λ r p q . p q ( λ m . Succ ( r m q ) ) {\displaystyle \qquad \operatorname {Add} =\operatorname {Y} \lambda rpq.p\ q\ (\lambda m.\operatorname {Succ} \,(r\ m\ q))}
Church numerals, on the other hand, already embody the primitive recursion and perform the folding / looping on their own:
A d d C h u r c h = λ p q s z . p s ( q s z ) {\displaystyle \qquad \operatorname {Add_{_{\,Church}}} =\lambda pqsz.p\ s\ (q\ s\ z)}
The key difference is that Scott's handler's argument is the number's own predecessor Scott numeral, unprocessed, whereas Church's folding / looping function's argument is the result of folding / looping over its predecessor.
Lists Scott encoding of lists follows their definition as a sum of two cases, the empty list case and the cons case,
L i s t := NIL | Cons ⟨ v a l ⟩ L i s t {\displaystyle \qquad List:=\operatorname {NIL} \ |\,\operatorname {Cons} \,\langle val\rangle \,List}
Correspondingly, Scott lists are functions which expect two arguments, two handlers, each receiving the corresponding data from the list:
NIL = λ n c . n Cons = λ a d . λ n c . c a d {\displaystyle \quad {\begin{aligned}\operatorname {NIL} &=\lambda nc.n\\\operatorname {Cons} &=\lambda ad.\lambda nc.c\ a\ d\end{aligned}}}
… excerpt ends here. Continue reading the full article.
