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:
“The great challenge which faces us is to assure that, in our society of big-ness, we do not strangle the voice of creativity, that the rules of the game do not come to overshadow its purpose, that the grand orchestration of society leaves ample room for the man who marches to the music of another drummer.”
—Hubert H. Humphrey (1911–1978)