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:

    “One might get the impression that I recommend a new methodology which replaces induction by counterinduction and uses a multiplicity of theories, metaphysical views, fairy tales, instead of the customary pair theory/observation. This impression would certainly be mistaken. My intention is not to replace one set of general rules by another such set: my intention is rather to convince the reader that all methodologies, even the most obvious ones, have their limits.”
    —Paul Feyerabend (1924–1994)