Typing Rules
To define the set of well typed lambda terms of a given type, we will define a typing relation between terms and types. First, we introduce typing contexts or typing environments, which are sets of typing assumptions. A typing assumption has the form, meaning has type .
The typing relation indicates that is a term of type in context . It is therefore said that " is well-typed (at )". Instances of the typing relation are called typing judgements. The validity of a typing judgement is shown by providing a typing derivation, constructed using typing rules (wherein the premises above the line allow us to derive the conclusion below the line). Simply-typed lambda calculus uses these rules:
| (1) (2) |
| (3) (4) |
In other words,
- If has type in the context, we know that has type .
- Term constants have the appropriate base types.
- If, in a certain context with having type, has type, then, in the same context without, has type .
- If, in a certain context, has type, and has type, then has type .
Examples of closed terms, i.e. terms typable in the empty context, are:
- For every type, a term (the I-combinator/identity function),
- For types, a term (the K-combinator), and
- For types, a term (the S-combinator).
These are the typed lambda calculus representations of the basic combinators of combinatory logic.
Each type is assigned an order, a number . For base types, ; for function types, . That is, the order of a type measures the depth of the most left-nested arrow. Hence:
Read more about this topic: Simply Typed Lambda Calculus
Famous quotes containing the word rules:
“But suppose, asks the student of the professor, we follow all your structural rules for writing, what about that “something else” that brings the book alive? What is the formula for that? The formula for that is not included in the curriculum.”
—Fannie Hurst (1889–1968)