Simply Typed Lambda Calculus - Typing Rules

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,

  1. If has type in the context, we know that has type .
  2. Term constants have the appropriate base types.
  3. If, in a certain context with having type, has type, then, in the same context without, has type .
  4. 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:

    For rhetoric, he could not ope
    His mouth, but out there flew a trope;
    And when he happen’d to break off
    I’ th’ middle of his speech, or cough,
    H’ had hard words ready to show why,
    And tell what rules he did it by;
    Samuel Butler (1612–1680)