Definition 6 (Types) The set of types is the smallest set such that:
1. al l basic types are types;
2. if α and β are types then α → β and α × β are types.
Each type may correspond to a set of objects of that type. In this way
hierarchies of type domains, called (standard) frames are obtained.
Definition 7 (Standard Frames) A (standard) frame is a set of non-empty
sets {Dα | α is a type} such that, for all α, β
Dt = {0, 1};
Dα→β = Dα → Dβ ;
Dα×β = Dα × Dβ.
Frames will be the backbones of our models. We shall use them in order to
interpret the language which we are about to define. For each type α, let us
assume the existence of a denumerably infinite set of variables V ARα and
some set of constants CONα . From these basic terms complex ones can be
built.
Definition 8 (Terms) Define, for each α, the set Tα of terms of type α by
the following induction.
1. CONα ⊆ Tα, VARα ⊆ Tα;
2. A ∈ Tα→β, B∈Tα ⇒ A(B) ∈Tβ;
3. A∈Tβ, ξ∈VARα⇒λξ.A∈Tα→β;
4. A∈Tα, B∈Tβ⇒ hA, Bi ∈ Tα×β;
5. A∈ Tα×β ⇒ (A)0 ∈Tα and (A)1 ∈ Tβ;
6. A∈Tα, B∈Tα⇒ (A=B) ∈Tt.
If A ∈ Tα we may (but need not) indicate this by writing Aα . Terms of type
t are called formulae. In (A)0 and (A)1 the parentheses are often omitted if
this is not likely to lead to confusion. Note that the first five clauses in the
above definition give the syntax of a simply typed λ-calculus with pairing and
10
More intriguing information
1. The name is absent2. Modelling the Effects of Public Support to Small Firms in the UK - Paradise Gained?
3. Lumpy Investment, Sectoral Propagation, and Business Cycles
4. Can a Robot Hear Music? Can a Robot Dance? Can a Robot Tell What it Knows or Intends to Do? Can it Feel Pride or Shame in Company?
5. Eigentumsrechtliche Dezentralisierung und institutioneller Wettbewerb
6. Needing to be ‘in the know’: strategies of subordination used by 10-11 year old school boys
7. Testing the Information Matrix Equality with Robust Estimators
8. BARRIERS TO EFFICIENCY AND THE PRIVATIZATION OF TOWNSHIP-VILLAGE ENTERPRISES
9. HOW WILL PRODUCTION, MARKETING, AND CONSUMPTION BE COORDINATED? FROM A FARM ORGANIZATION VIEWPOINT
10. The name is absent