Program Semantics and Classical Logic



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 absent
2. he Effect of Phosphorylation on the Electron Capture Dissociation of Peptide Ions
3. The name is absent
4. Education as a Moral Concept
5. Passing the burden: corporate tax incidence in open economies
6. The name is absent
7. Fiscal Rules, Fiscal Institutions, and Fiscal Performance
8. The name is absent
9. A MARKOVIAN APPROXIMATED SOLUTION TO A PORTFOLIO MANAGEMENT PROBLEM
10. Peer Reviewed, Open Access, Free
11. Une nouvelle vision de l'économie (The knowledge society: a new approach of the economy)
12. Naïve Bayes vs. Decision Trees vs. Neural Networks in the Classification of Training Web Pages
13. Lending to Agribusinesses in Zambia
14. Human Rights Violations by the Executive: Complicity of the Judiciary in Cameroon?
15. Impact of Ethanol Production on U.S. and Regional Gasoline Prices and On the Profitability of U.S. Oil Refinery Industry
16. Imputing Dairy Producers' Quota Discount Rate Using the Individual Export Milk Program in Quebec
17. Does adult education at upper secondary level influence annual wage earnings?
18. Voting by Committees under Constraints
19. Assessing Economic Complexity with Input-Output Based Measures
20. The name is absent