Page 35 - Textos de Matemática Vol. 40

1.4. Models 23 Definition 1.4.1. Let ρ be the reduction relation defined by the following clauses
for all closed terms t, s, and r of Lp and natural numbers n and m, n ̸= m.
kts ρ t, (1) stsr ρ tr(sr), (2) p0(pts) ρ t, (3) p1(pts) ρ s, (4) pN(sNn) ρ n, (5) dNtsnn ρ t, (6) dNtsnm ρ s. (7)
Of course, the relation ρ may be extended to new constants and their corresponding rewrite rules. For instance, in the presence of primitive recursion we have to add the two clauses:
rNtsr0 ρ t0r, (8) rN tsrn+1 ρ sr(rN tsrn). (9)
Normal term models. Let ρ + be the relation generated by ρ according to the leftmost minimal strategy. That means, in every reduction step of a term t we reduce the leftmost subterm of t which does not contain a subterm reducible by ρ .
Terms which are irreducible with respect to ρ + are called in normal form.
Now we can define the closed normal term model, CNT. We choose as universe the set of closed terms which are in normal form with respect to ρ +. The constants of BON are interpreted by themselves and applications of the form t s of closed terms t and s are interpreted by the (uniquely determined) normal form of ts with respect to ρ +, if it exists. Equality is interpreted as literal identity and N as the set of numerals n, n ∈ IN.
Proposition 1.4.2. [Bee85, Theorem VI.6.1.3] CN T |= BON.
Total term models. For the total term model, CT T , the universe consists of all closed terms of the language. Therefore, we can interprete the constants by themselves, and application by juxtaposition. Two terms are equal if they have a common reduct with respect to arbitrary reductions on the basis of ρ. Here, it is needed to prove the Church-Rosser property to verify transitivity of equality. Finally, N(t) holds if t reduces to a numeral.
In the model CT T totality, (Tot), is satisfied, i.e., the application of t and s is always defined in the sense of ↓. Thus CT T can be considered as the standard model for total applicative theories.
Proposition 1.4.3. [Bee85, Theorem VI.6.2.1] CT T |= BON + (Tot).