Page 62 - Textos de Matemática Vol. 40

50 Chapter 1. Applicative theories
Definition 1.8.6. Let A1,...,An,B1,...,Bn be classes. Furthermore, let T be the class (A1 B1) ∩ ··· ∩ (An Bn). Then T is called an arrow class. We define:
r⊑s := r↓→r=s,
f1 x ≃ 1 if x = 1, notN otherwise
Now we let g be the operation

f1 f2
notN
1 otherwise.
gx≃
if x = f1, otherwise.

f⊑T g :=
f∼=T g := f⊑T g∧g⊑T f.
The formula r ⊑ s ∧ s ⊑ r is equivalent to the standard partial equality relation r ≃ s. Hence, our definedness ordering ⊑ is in accordance with the notion of partiality of our applicative theory. Studer [Stu01a] employs a least fixed point operator to define a denotational semantics for featherweight java. This semantics features an overloading based object model. An over- loaded function models type-dependent computations and hence, it belongs to the intersection of several function spaces. Therefore, we define arrow types to be such intersections in order to prepare our setting for this application.
The relations ⊑ and ⊑T are transitive.
Lemma 1.8.7. Let T be an arrow class as given in Definition 1.8.6. Then we
can prove in LFP:
1. r⊑s∧s⊑t→r⊑t,
2. f⊑T g∧g⊑T h→f⊑T h.
Proof. Wehaver↓→r=saswellass↓→s=t. Obviouslywegetr↓→r= t proving Claim 1. Now we show the second Claim. Assume x ∈ Ai for some i. Wehavefx⊑gxandgx⊑hx. Therefore,weconcludefx⊑hxbythefirst Claim. ⊣
Using the rec term we will find a fixed point for every operation g. But as mentioned before we cannot prove that this is a least fixed point; and of course, there are terms g that do not have a least fixed point.
Example 1.8.8. Let f1 and f2 be closed terms so that
1≤i≤n
∀x∈Ai.fx⊑gx,
and f2 x ≃
if x = 1,
Let V be the universal class x = x. Then we know g ∈ ((VV) → (VV)), andiffisafixedpointofgthenwehaveeitherf=f1 or∀x.fx≃f2x.