The simply typed lambda calculus, a form of type theory, is a typed interpretation of the lambda calculus with only one type constructor: that builds function types. It is the canonical and simplest example of a typed lambda calculus. The simply typed lambda calculus was originally introduced by Alonzo Church in 1940 as an attempt to avoid paradoxical uses of the untyped lambda calculus, and it exhibits many desirable and interesting properties.
The term simple type is also used to refer to extensions of the simply typed lambda calculus such as products, coproducts or natural numbers (System T) or even full recursion (like PCF). In contrast, systems which introduce polymorphic types (like System F) or dependent types (like the Logical Framework) are not considered simply typed. The former are still considered simple because the Church encodings of such structures can be done using only and suitable type variables, while polymorphism and dependency cannot.
Read more about Simply Typed Lambda Calculus: Syntax, Typing Rules, Alternative Syntaxes, General Observations, Important Results
Famous quotes containing the words simply and/or calculus:
“The dissident does not operate in the realm of genuine power at all. He is not seeking power. He has no desire for office and does not gather votes. He does not attempt to charm the public, he offers nothing and promises nothing. He can offer, if anything, only his own skin—and he offers it solely because he has no other way of affirming the truth he stands for. His actions simply articulate his dignity as a citizen, regardless of the cost.”
—Václav Havel (b. 1936)
“I try to make a rough music, a dance of the mind, a calculus of the emotions, a driving beat of praise out of the pain and mystery that surround me and become me. My poems are meant to make your mind get up and shout.”
—Judith Johnson Sherwin (b. 1936)