DynBindModelExamples: Difference between revisions

Latest revision as of 10:11, 11 April 2007

Template:Article will be deleted Author: Matthias Konrad

The system

In this example we are studying a simple system with three classes that contains both renaming and selects:

class
   A
feature
   f1 do ... end
   g1 do ... end
end

class
   B
inherit
   A
      rename f1 as f2, g1 as g2 
      redefine f2, g2 end
feature
   f2 do ... end
   g2 do ... end
end

class
   D
inherit
 
   A
      redefine f1, g1 
      select g1 end
   B
      select f2 end
feature
   f1 do ... end
   g1 do ... end
end

This system is defined by:

$S = {A, B, D}$

$τ = {A \mapsto {f 1 \mapsto \underline{A . f 1}, g 1 \mapsto \underline{A . g 1}}, B \mapsto {f 2 \mapsto \underline{B . f 2}, g 2 \mapsto \underline{B . g 2}}, D \mapsto {f 1 \mapsto \underline{D . f 1}, g 1 \mapsto \underline{D . g 1}}}$

$α = {A \mapsto \emptyset, B \mapsto {A}, D \mapsto {A, B}}$

$η = {A \mapsto \emptyset, B \mapsto {A \mapsto {f_{1} \mapsto f_{2}, g_{1} \mapsto g_{2}}}, D \mapsto {A \mapsto \emptyset, B \mapsto \emptyset}}$

$σ = {A \mapsto \emptyset, B \mapsto {A \mapsto \emptyset}, D \mapsto {A \mapsto {g_{1}}, B \mapsto {f_{2}}}}$

$C = {1 \mapsto A, 2 \mapsto B, 3 \mapsto D}$

The naming function

We proceed by calculating the naming function. According to its definition we have to do that incrementally. Meaning that we first calculate $β_{S_{1}}$ then $β_{S_{2}}$ and finally $β_{S_{3}}$ .

Calculating $β_{S_{1}}$

Since $β_{S_{1}}$ contains only one class it is sufficient to define $β_{S_{1}} (A \mapsto A)$ . According to the definition:

$β_{S_{1}} (C_{1} \mapsto C_{1}) = id (dom (τ_{1}) \cup UNION b \cdot (b \in α_{1} | ran (β_{S_{0}} (b \mapsto b) ≪ η_{1, b})))$

We can forget about the right part of the union since $C_{1}$ has no base classes. So we need to calculate:

id(dom(τ1))
1. $τ_{1} = τ (C_{1}) = {f_{1} \mapsto \underline{C_{1} . f_{1}}, g_{1} \mapsto \underline{C_{1} . g_{1}}}$
2. $dom (τ_{1}) = {f_{1}, g_{1}}$
3. $id (dom (τ_{1})) = {f_{1} \mapsto f_{1}, g_{1} \mapsto g_{1}}$

So we get:

$β_{S_{1}} (C_{1} \mapsto C_{1}) = {f_{1} \mapsto f_{1}, g_{1} \mapsto g_{1}}$

And hence:

$β_{S_{1}} = {(C_{1} \mapsto C_{1}) \mapsto {f_{1} \mapsto f_{1}, g_{1} \mapsto g_{1}}}$

Calculating $β_{S_{2}}$

We show the calculation of the different (four) parts of the function in separate sections:

Calculate $β_{S_{2}} (C_{1} \mapsto C_{1})$

According to the definition: $β_{S_{2}} (C_{1} \mapsto C_{1}) = β_{S_{1}} (C_{1} \mapsto C_{1}) = {f_{1} \mapsto f_{1}, g_{1} \mapsto g_{1}}$

Calculate $β_{S_{2}} (C_{2} \mapsto C_{1})$

According to the definition: $β_{S_{2}} (C_{2} \mapsto C_{1}) = \emptyset$

Calculate $β_{S_{2}} (C_{2} \mapsto C_{2})$

According to the definition: $β_{S_{2}} (C_{2} \mapsto C_{2}) = id (dom (τ_{2}) \cup UNION b \cdot (b \in α_{2} | ran (β_{S_{1}} (b \mapsto b) ≪ η_{2, b})))$

Lets calculate the left part first:

$τ_{2} = τ (C_{2}) = {f_{2} \mapsto \underline{C_{2} . f_{2}}, g_{2} \mapsto \underline{C_{2} . g_{2}}}$
$dom (τ_{2}) = {f_{2}, g_{2}}$

And now the right part:

$UNION b \cdot (b \in {C_{1}} | ran (β_{S_{1}} (b \mapsto b) ≪ η_{2, b})) = ran (β_{S_{1}} (C_{1} \mapsto C_{1}) ≪ η_{2, C_{1}})$
$β_{S_{1}} (C_{1} \mapsto C_{1}) = {f_{1} \mapsto f_{1}, g_{1} \mapsto g_{1}}$
$η_{2, C_{1}} = η (C_{2}) (C_{1}) = {f_{1} \mapsto f_{2}, g_{1} \mapsto g_{2}}$
${f_{1} \mapsto f_{1}, g_{1} \mapsto g_{1}} ≪ {f_{1} \mapsto f_{2}, g_{1} \mapsto g_{2}} = {f_{1} \mapsto f_{2}, g_{1} \mapsto g_{2}}$
$ran ({f_{1} \mapsto f_{2}, g_{1} \mapsto g_{2}}) = {f_{2}, g_{2}}$

So we get:

$β_{S_{2}} (C_{2} \mapsto C_{2}) = {f_{2} \mapsto f_{2}, g_{2} \mapsto g_{2}}$

Calculate $β_{S_{2}} (C_{1} \mapsto C_{2})$

According to the definition: $β_{S_{2}} (C_{1} \mapsto C_{2}) = {β_{S_{2}}}^{'} (C_{1} \mapsto C_{2}) ≪ θ_{S_{2}} (C_{1} \mapsto C_{2})$

Where: ${β_{S_{2}}}^{'} (C_{1} \mapsto C_{2}) = UNION b \cdot (b \in α_{2} | β_{S_{1}} (C_{1} \mapsto b); (id (ran (β_{S_{1}} (C_{1} \mapsto b))) ≪ η_{2, b}))$

And: $θ_{S_{2}} (C_{1} \mapsto C_{2}) = UNION b \cdot (b \in α_{2} | β_{S_{1}} (C_{1} \mapsto b); (id (ran (β_{S_{1}} (C_{1} \mapsto b))) ≪ η_{2, b}) ▹ σ_{2, b})$

Here are the steps taken to compute the part:

βS1(C1↦C1);(id(ran(βS1(C1↦C1)))≪η2,C1)
1. $id (ran (β_{S_{1}} (C_{1} \mapsto C_{1}))) = {f_{1} \mapsto f_{1}, g_{1} \mapsto g_{1}}$
2. ${f_{1} \mapsto f_{1}, g_{1} \mapsto g_{1}} ≪ {f_{1} \mapsto f_{2}, g_{1} \mapsto g_{2}} = {f_{1} \mapsto f_{2}, g_{1} \mapsto g_{2}}$
3. ${f_{1} \mapsto f_{1}, g_{1} \mapsto g_{1}}; {f_{1} \mapsto f_{2}, g_{1} \mapsto g_{2}} = {f_{1} \mapsto f_{2}, g_{1} \mapsto g_{2}}$
4. ${β_{S_{2}}}^{'} (C_{1} \mapsto C_{2}) = {f_{1} \mapsto f_{2}, g_{1} \mapsto g_{2}}$
βS1(C1↦C1);(id(ran(βS1(C1↦C1)))≪η2,C1)▹σ2,C1
1. $σ_{2, C_{1}} = \emptyset$
2. $id (ran (β_{S_{1}} (C_{1} \mapsto C_{1}))) ≪ \emptyset = \emptyset$
3. $β_{S_{1}} (C_{1} \mapsto C_{1}); \emptyset = \emptyset$
4. $θ_{S_{2}} (C_{1} \mapsto C_{2}) = \emptyset$
${f_{1} \mapsto f_{2}, g_{1} \mapsto g_{2}} ≪ \emptyset = {f_{1} \mapsto f_{2}, g_{1} \mapsto g_{2}}$

So we get:

$β_{S_{2}} (C_{1} \mapsto C_{2}) = {f_{1} \mapsto f_{2}, g_{1} \mapsto g_{2}}$

Putting the parts together:

We can know show the complete total function:

$β_{S_{2}} = {$	$(C_{1} \mapsto C_{1}) \mapsto {f_{1} \mapsto f_{1}, g_{1} \mapsto g_{1}},$
	$(C_{1} \mapsto C_{2}) \mapsto {f_{1} \mapsto f_{2}, g_{1} \mapsto g_{2}},$
	$(C_{2} \mapsto C_{1}) \mapsto \emptyset,$
	$(C_{2} \mapsto C_{2}) \mapsto {f_{2} \mapsto f_{2}, g_{2} \mapsto g_{2}}}$

Calculating $β_{S_{3}}$

We will not show the complete construction of $β_{S_{3}}$ but restrict our self to the most interesting parts.

Calculate $β_{S_{3}} (C_{1} \mapsto C_{3})$

According to the definition: $β_{S_{3}} (C_{1} \mapsto C_{3}) = {β_{S_{3}}}^{'} (C_{1} \mapsto C_{3}) ≪ θ_{S_{3}} (C_{1} \mapsto C_{3})$

Where: ${β_{S_{3}}}^{'} (C_{1} \mapsto C_{3}) = UNION b \cdot (b \in α_{3} | β_{S_{2}} (C_{1} \mapsto b); (id (ran (β_{S_{2}} (C_{1} \mapsto b))) ≪ η_{3, b}))$

And: $θ_{S_{3}} (C_{1} \mapsto C_{3}) = UNION b \cdot (b \in α_{3} | β_{S_{2}} (C_{1} \mapsto b); (id (ran (β_{S_{2}} (C_{1} \mapsto b))) ≪ η_{3, b}) ▹ σ_{3, b})$

Note that we can omit $η_{3, b}$ from the formulas since it is always empty.

βS2(C1↦C2);id(ran(βS2(C1↦C2))) ∪ βS2(C1↦C1);id(ran(βS2(C1↦C1)))
1. $β_{S_{2}} (C_{1} \mapsto C_{2}) = {f_{1} \mapsto f_{2}, g_{1} \mapsto g_{2}}$
2. $id (ran (β_{S_{2}} (C_{1} \mapsto C_{2}))) = {f_{2} \mapsto f_{2}, g_{2} \mapsto g_{2}}$
3. $β_{S_{2}} (C_{1} \mapsto C_{2}); id (ran (β_{S_{2}} (C_{1} \mapsto C_{2}))) = {f_{1} \mapsto f_{2}, g_{1} \mapsto g_{2}}$
4. $β_{S_{2}} (C_{1} \mapsto C_{1}) = {f_{1} \mapsto f_{1}, g_{1} \mapsto g_{1}}$
5. $id (ran (β_{S_{2}} (C_{1} \mapsto C_{1}))) = {f_{1} \mapsto f_{1}, g_{1} \mapsto g_{1}}$
6. $β_{S_{2}} (C_{1} \mapsto C_{1}); id (ran (β_{S_{2}} (C_{1} \mapsto C_{1}))) = {f_{1} \mapsto f_{1}, g_{1} \mapsto g_{1}}$
7. ${f_{1} \mapsto f_{2}, g_{1} \mapsto g_{2}} \cup {f_{1} \mapsto f_{1}, g_{1} \mapsto g_{1}} = {f_{1} \mapsto f_{1}, f_{1} \mapsto f_{2}, g_{1} \mapsto g_{1}, g_{1} \mapsto g_{2}}$
βS2(C1↦C2);id(ran(βS2(C1↦C2))) ▹ σ3,C2 ∪ βS2(C1↦C1);id(ran(βS2(C1↦C1))) ▹ σ3,C1
1. $σ_{3, C_{2}} = σ (C_{3}) (C_{2}) = {f_{2}}$
2. $σ_{3, C_{1}} = σ (C_{3}) (C_{1}) = {g_{1}}$
3. $β_{S_{2}} (C_{1} \mapsto C_{2}); id (ran (β_{S_{2}} (C_{1} \mapsto C_{2}))) ▹ σ_{3, C_{2}} = {f_{1} \mapsto f_{2}}$
4. $β_{S_{2}} (C_{1} \mapsto C_{1}); id (ran (β_{S_{2}} (C_{1} \mapsto C_{1}))) ▹ σ_{3, C_{1}} = {g_{1} \mapsto g_{1}}$
5. ${f_{1} \mapsto f_{2}} \cup {g_{1} \mapsto g_{1}} = {f_{1} \mapsto f_{2}, g_{1} \mapsto g_{1}}$
6. ${f_{1} \mapsto f_{1}, f_{1} \mapsto f_{2}, g_{1} \mapsto g_{1}, g_{1} \mapsto g_{2}} ≪ {f_{1} \mapsto f_{2}, g_{1} \mapsto g_{1}} = {f_{1} \mapsto f_{2}, g_{1} \mapsto g_{1}}$

So we get:

$β_{S_{3}} (C_{1} \mapsto C_{3}) = {f_{1} \mapsto f_{2}, g_{1} \mapsto g_{1}}$

The complete naming function

$β_{S_{3}} = {$	$(C_{1} \mapsto C_{1}) \mapsto {f_{1} \mapsto f_{1}, g_{1} \mapsto g_{1}},$
	$(C_{1} \mapsto C_{2}) \mapsto {f_{1} \mapsto f_{2}, g_{1} \mapsto g_{2}},$
	$(C_{2} \mapsto C_{1}) \mapsto \emptyset,$
	$(C_{2} \mapsto C_{2}) \mapsto {f_{2} \mapsto f_{2}, g_{2} \mapsto g_{2}},$
	$(C_{1} \mapsto C_{3}) \mapsto {f_{1} \mapsto f_{2}, g_{1} \mapsto g_{1}},$
	$(C_{2} \mapsto C_{3}) \mapsto {f_{2} \mapsto f_{2}, g_{2} \mapsto g_{2}},$
	$(C_{3} \mapsto C_{3}) \mapsto {f_{1} \mapsto f_{1}, g_{1} \mapsto g_{1}, f_{2} \mapsto f_{2}, g_{2} \mapsto g_{2}},$
	$(C_{3} \mapsto C_{1}) \mapsto \emptyset,$
	$(C_{3} \mapsto C_{2}) \mapsto \emptyset}$

The dynamic binding function

To calculate the dynamic binding function, we need to get $δ_{S_{3}}$ . We will again calculate it incrementally:

Calculating $δ_{S_{1}}$

According to the definition:

$δ_{S_{1}} (C_{1} \mapsto C_{1}) = β_{S} (C_{1} \mapsto C_{1}); ((UNION b \cdot (b \in α_{1} | {(β_{S} (b \mapsto b); η_{1, b})}^{- 1}; δ_{S_{0}} (b \mapsto b))) ≪ τ_{1})$

Since $α_{1}$ is empty this simplifies to: $δ_{S_{1}} (C_{1} \mapsto C_{1}) = β_{S} (C_{1} \mapsto C_{1}); τ_{1} = {f_{1} \mapsto f_{1}, g_{1} \mapsto g_{1}}; {f_{1} \mapsto \underline{C_{1} . f_{1}}, g_{1} \mapsto \underline{C_{1} . g_{1}}}$

So we get: $δ_{S_{1}} = {(C_{1} \mapsto C_{1}) \mapsto {f_{1} \mapsto \underline{C_{1} . f_{1}}, g_{1} \mapsto \underline{C_{1} . g_{1}}}}$

Calculating $δ_{S_{2}}$

Again we calculate the different parts of the function in separate sections:

Calculate $δ_{S_{2}} (C_{1} \mapsto C_{1})$

According to the definition: $δ_{S_{2}} (C_{1} \mapsto C_{1}) = δ_{S_{1}} (C_{1} \mapsto C_{1}) = {f_{1} \mapsto \underline{C_{1} . f_{1}}, g_{1} \mapsto \underline{C_{1} . g_{1}}}$

Calculate $δ_{S_{2}} (C_{2} \mapsto C_{1})$

According to the definition: $δ_{S_{2}} (C_{1} \mapsto C_{1}) = \emptyset$

Calculate $δ_{S_{2}} (C_{2} \mapsto C_{2})$

According to the definition:

$δ_{S_{2}} (C_{2} \mapsto C_{2}) = β_{S} (C_{2} \mapsto C_{2}); ((UNION b \cdot (b \in α_{2} | {(β_{S} (b \mapsto b); η_{2, b})}^{- 1}; δ_{S_{1}} (b \mapsto b))) ≪ τ_{2})$

UNIONb⋅(b∈{C1}|(βS(b↦b);η2,b)−1;δS1(b↦b))=(βS(C1↦C1);η2,C1)−1;δS1(C1↦C1)
1. $β_{S} (C_{1} \mapsto C_{1}); η_{2, C_{1}} = {f_{1} \mapsto f_{2}, g_{1} \mapsto g_{2}}$
2. ${(β_{S} (C_{1} \mapsto C_{1}); η_{2, C_{1}})}^{- 1} = {f_{2} \mapsto f_{1}, g_{2} \mapsto g_{1}}$
3. ${(β_{S} (C_{1} \mapsto C_{1}); η_{2, C_{1}})}^{- 1}; δ_{S_{1}} (C_{1} \mapsto C_{1}) = {f_{2} \mapsto \underline{C_{1} . f_{1}}, g_{2} \mapsto \underline{C_{1} . g_{1}}}$
$τ_{2} = τ (C_{2}) = {f_{2} \mapsto \underline{C_{2} . f_{2}}, g_{2} \mapsto \underline{C_{2} . g_{2}}}$
${f_{2} \mapsto \underline{C_{1} . f_{1}}, g_{2} \mapsto \underline{C_{1} . g_{1}}} ≪ {f_{2} \mapsto \underline{C_{2} . f_{2}}, g_{2} \mapsto \underline{C_{2} . g_{2}}} = {f_{2} \mapsto \underline{C_{2} . f_{2}}, g_{2} \mapsto \underline{C_{2} . g_{2}}}$

So we get: $δ_{S_{2}} (C_{2} \mapsto C_{2}) = {f_{2} \mapsto \underline{C_{2} . f_{2}}, g_{2} \mapsto \underline{C_{2} . g_{2}}}$

Calculate $δ_{S_{2}} (C_{1} \mapsto C_{2})$

According to the definition:

$δ_{S_{2}} (C_{1} \mapsto C_{2}) = β_{S} (C_{1} \mapsto C_{2}); ((UNION b \cdot (b \in α_{2} | {(β_{S} (b \mapsto b); η_{2, b})}^{- 1}; δ_{S_{1}} (b \mapsto b))) ≪ τ_{2})$

At this stage it should be clear how to calculate this, so we just give the result:

$δ_{S_{2}} (C_{1} \mapsto C_{2}) = {f_{1} \mapsto \underline{C_{2} . f_{2}}, g_{1} \mapsto \underline{C_{2} . g_{2}}}$

Putting the parts together:

We can know show the complete total function:

$δ_{S_{2}} = {$	$(C_{1} \mapsto C_{1}) \mapsto {f_{1} \mapsto \underline{C_{1} . f_{1}}, g_{1} \mapsto \underline{C_{1} . g_{1}}},$
	$(C_{1} \mapsto C_{2}) \mapsto {f_{1} \mapsto \underline{C_{2} . f_{2}}, g_{1} \mapsto \underline{C_{2} . g_{2}}},$
	$(C_{2} \mapsto C_{1}) \mapsto \emptyset,$
	$(C_{2} \mapsto C_{2}) \mapsto {f_{2} \mapsto \underline{C_{2} . f_{2}}, g_{2} \mapsto \underline{C_{2} . g_{2}}}}$

Calculating $δ_{S_{3}}$

There is nothing new for this calculation so we just present the result:

$δ_{S_{3}} = {$	$(C_{1} \mapsto C_{1}) \mapsto {f_{1} \mapsto \underline{C_{1} . f_{1}}, g_{1} \mapsto \underline{C_{1} . g_{1}}},$
	$(C_{1} \mapsto C_{2}) \mapsto {f_{1} \mapsto \underline{C_{2} . f_{2}}, g_{1} \mapsto \underline{C_{2} . g_{2}}},$
	$(C_{2} \mapsto C_{1}) \mapsto \emptyset,$
	$(C_{2} \mapsto C_{2}) \mapsto {f_{2} \mapsto \underline{C_{2} . f_{2}}, g_{2} \mapsto \underline{C_{2} . g_{2}}},$
	$(C_{1} \mapsto C_{3}) \mapsto {f_{1} \mapsto \underline{C_{2} . f_{2}}, g_{1} \mapsto \underline{C_{3} . g_{1}}},$
	$(C_{2} \mapsto C_{3}) \mapsto {f_{2} \mapsto \underline{C_{2} . f_{2}}, g_{2} \mapsto \underline{C_{2} . g_{2}}},$
	$(C_{3} \mapsto C_{3}) \mapsto {f_{1} \mapsto \underline{C_{3} . f_{1}}, g_{1} \mapsto \underline{C_{3} . g_{1}}, f_{2} \mapsto \underline{C_{2} . f_{2}}, g_{2} \mapsto \underline{C_{2} . g_{2}}},$
	$(C_{3} \mapsto C_{1}) \mapsto \emptyset,$
	$(C_{3} \mapsto C_{2}) \mapsto \emptyset}$

Deriving the dynamic binding function

The function is now given. We evaluate it at two interesting points:

$δ (C_{1} \mapsto f_{1}) = {C_{1} \mapsto \underline{C_{1} . f_{1}}, C_{2} \mapsto \underline{C_{2} . f_{2}}, C_{3} \mapsto \underline{C_{2} . f_{2}}}$

$δ (C_{1} \mapsto f_{g}) = {C_{1} \mapsto \underline{C_{1} . f_{g}}, C_{2} \mapsto \underline{C_{2} . g_{2}}, C_{3} \mapsto \underline{C_{2} . g_{1}}}$

DynBindModelExamples: Difference between revisions

Latest revision as of 10:11, 11 April 2007

Contents

The system

The naming function

Calculating $β_{S_{1}}$

Calculating $β_{S_{2}}$

Calculate $β_{S_{2}} (C_{1} \mapsto C_{1})$

Calculate $β_{S_{2}} (C_{2} \mapsto C_{1})$

Calculate $β_{S_{2}} (C_{2} \mapsto C_{2})$

Calculate $β_{S_{2}} (C_{1} \mapsto C_{2})$

Putting the parts together:

Calculating $β_{S_{3}}$

Calculate $β_{S_{3}} (C_{1} \mapsto C_{3})$

The complete naming function

The dynamic binding function

Calculating $δ_{S_{1}}$

Calculating $δ_{S_{2}}$

Calculate $δ_{S_{2}} (C_{1} \mapsto C_{1})$

Calculate $δ_{S_{2}} (C_{2} \mapsto C_{1})$

Calculate $δ_{S_{2}} (C_{2} \mapsto C_{2})$

Calculate $δ_{S_{2}} (C_{1} \mapsto C_{2})$

Putting the parts together:

Calculating $δ_{S_{3}}$

Deriving the dynamic binding function

Navigation menu

@@ Line 1: / Line 1: @@
-This page shows
+[[Category:ECMA]]
+{{Article will be deleted}}
+Author: Matthias Konrad[[Category:ECMA]]
-=Example 1=
 ==The system==
-In this example we are studying a symple system with three classes that contains both renaming and selects:
+In this example we are studying a simple system with three classes that contains both renaming and selects:
 {|border="0" cellpadding="2" cellspacing="0" align="center"
@@ Line 9: / Line 10: @@
 |<code>[eiffel, N]
 class
-    C1
+    A
 feature
     f1 do ... end
@@ Line 18: / Line 19: @@
 <code>[eiffel, N]
 class
-    C2
+    B
 inherit
-    B
+    A
        rename f1 as f2, g1 as g2
        redefine f2, g2 end
@@ Line 31: / Line 32: @@
 <code>[eiffel, N]
 class
-    C3
+    D
 inherit
-    C2
-      select f1 end
+    A
-    C1
        redefine f1, g1
        select g1 end
+   B
+      select f2 end
 feature
     f1 do ... end
@@ Line 45: / Line 47: @@
 |}
 This system is defined by:
-*<math>S = \left\{ C_1, C_2, C_3 \right\} </math>
-*<math>S_1 = \left\{ C_1\right\}, S_2 = \left\{ C_1, C_2\right\}, S_3 = \left\{ C_1, C_2, C_3 \right\}</math>
+<math>S=\left\{ A, B, D\right\}</math>
-*<math>\tau =
+<math>\tau =
 \left\{
-    C_1 \mapsto \left\{ f_1 \mapsto \underline{C_1.f_1}, g_1 \mapsto \underline{C_1.g_1} \right\},
+    A \mapsto \left\{ f1 \mapsto \underline{A.f1}, g1 \mapsto \underline{A.g1} \right\},
-    C_2 \mapsto \left\{ f_2 \mapsto \underline{C_2.f_2}, g_2 \mapsto \underline{C_2.g_2} \right\},
+    B \mapsto \left\{ f2 \mapsto \underline{B.f2}, g2 \mapsto \underline{B.g2} \right\},
-    C_3 \mapsto \left\{ f_1 \mapsto \underline{C_3.f_1}, g_1 \mapsto \underline{C_3.g_1} \right\}
+    D \mapsto \left\{ f1 \mapsto \underline{D.f1}, g1 \mapsto \underline{D.g1} \right\}
 \right\}
 </math>
-*<math>\eta =
+<math>\alpha = \left\{
+   A \mapsto \emptyset,
+   B \mapsto \left\{ A \right\},
+   D \mapsto \left\{ A, B \right\}
+\right\}
+</math>
+<math>\eta =
 \left\{
-    C_2 \mapsto \left\{
+    A \mapsto \emptyset,
-       C_1 \mapsto \left\{ f_1 \mapsto f_2, g_1 \mapsto g_2 \right\}
+   B \mapsto \left\{
+       A \mapsto \left\{ f_1 \mapsto f_2, g_1 \mapsto g_2 \right\}
+   \right\},
+   D \mapsto \left\{
+      A \mapsto \emptyset, B \mapsto \emptyset
     \right\}
 \right\}
 </math>
-*<math>\alpha = \left\{
-    C_2 \mapsto \left\{ C_1 \right\},
+<math>\sigma = \left\{
-    C_3 \mapsto \left\{ C_2, C_1 \right\}
+    A \mapsto \emptyset,
+   B \mapsto \left\{ A \mapsto \emptyset \right\},
+    D \mapsto \left\{ A \mapsto \left\{ g_1 \right\},
+                     B \mapsto \left\{ f_2 \right\} \right\}
 \right\}
 </math>
-*<math>\sigma = \left\{
-   C_3 \mapsto \left\{ C_2 \mapsto \left\{ f_1 \right\}, C_2 \mapsto \left\{ g_1 \right\} \right\}
+<math>
-\right\}
+   C = \left\{ 1 \mapsto A, 2 \mapsto B, 3 \mapsto D \right\}
 </math>
 ==The naming function==
-We proceed by calculating the naming function. According to its definition we have to do that incrementaly. Meaning that we first calculate <math>\beta_{S_1}</math> then  <math>\beta_{S_2}</math> and finally <math>\beta_{S_3}</math>.
+We proceed by calculating the naming function. According to its definition we have to do that incrementally. Meaning that we first calculate <math>\beta_{S_1}</math> then  <math>\beta_{S_2}</math> and finally <math>\beta_{S_3}</math>.
+===Calculating <math>\beta_{S_1}</math>===
-===Calculating <math>\beta_{S_1}</math>===
+Since <math>\beta_{S_1}</math> contains only one class it is sufficient to define <math>\beta_{S_1}\left( A \mapsto A\right)</math>. According to the definition:
+*<math>
+   \beta_{S_1}\left( C_1 \mapsto C_1 \right)
+      =
+   \mbox{id} \left(
+      \mbox{dom} \left( \tau_1 \right)
+         \, \cup \,
+      \mbox {UNION} \ b \, \cdot \, \left(b \in \alpha_1
+         \ |\
+      \mbox{ran} \left( \beta_{ S_0 } \left( b \mapsto b \right) \ll \eta_{1, b} \right) \right) \right)
+</math>
+We can forget about the right part of the union since <math>C_1\,</math> has no base classes. So we need to calculate:
+#<math>\mbox{id} \left( \mbox{dom} \left( \tau_1 \right) \right) </math>
+##<math>
+\tau_1 = \tau (C_1) = \left\{ f_1 \mapsto \underline{C_1.f_1}, g_1 \mapsto \underline{C_1.g_1} \right\}
+</math>
+##<math>
+\mbox{dom} \left( \tau_1 \right) = \left\{ f_1, g_1 \right\}
+</math>
+##<math>
+\mbox{id} \left( \mbox{dom} \left( \tau_1 \right) \right) = \left\{ f_1 \mapsto f_1, g_1 \mapsto g_1\right\}
+</math>
+So we get:
+<math>
+   \beta_{S_1}\left( C_1 \mapsto C_1 \right) = \left\{ f_1 \mapsto f_1, g_1 \mapsto g_1\right\}
+</math>
+And hence:
+<math>
+   \beta_{S_1} = \left\{ \left( C_1 \mapsto C_1 \right) \mapsto
+      \left\{ f_1 \mapsto f_1, g_1 \mapsto g_1 \right\} \right\}
+</math>
+===Calculating <math>\beta_{S_2}</math>===
+We show the calculation of the different (four) parts of the function in separate sections:
+====Calculate <math>\beta_{S_2}\left( C_1 \mapsto C_1 \right)</math>====
+According to the [[DynBindModel#The_naming_function|definition]]:
+<math>
+   \beta_{S_2}\left( C_1 \mapsto C_1 \right) =
+   \beta_{S_1}\left( C_1 \mapsto C_1 \right) =  \left\{ f_1 \mapsto f_1, g_1 \mapsto g_1\right\}
+</math>
-Since <math>\beta_{S_1}</math> contains only one class it is sufficient to define <math>\beta_{S_1}\left( C_1 \mapsto C_1 \right)</math>. According to the definition:
+====Calculate <math>\beta_{S_2}\left( C_2 \mapsto C_1 \right)</math>====
+According to the [[DynBindModel#The_naming_function|definition]]:
+<math>
+   \beta_{S_2}\left( C_2 \mapsto C_1 \right) = \emptyset
+</math>
+====Calculate <math>\beta_{S_2}\left( C_2 \mapsto C_2 \right)</math>====
+According to the [[DynBindModel#The_naming_function|definition]]:
 <math>
-    \beta_{S_1}\left( C_1 \mapsto C_1 \right)
+    \beta_{S_2}\left( C_2 \mapsto C_2 \right)
        =
-    \mbox{id} \left( \mbox{dom} \left( \tau_1 \right) \right)
+    \mbox{id} \left( \mbox{dom} \left( \tau_2 \right)
        \, \cup \,
-    \mbox {UNION} \ b \, \cdot \, \left(b \in \alpha_1
+    \mbox {UNION} \ b \, \cdot \, \left(b \in \alpha_2
+      \ |\
+   \mbox{ran}\left( \beta_{ S_{1} } \left( b \mapsto b \right) \ll \eta_{2, b} \right)\right)
+   \right)
+</math>
+Lets calculate the left part first:
+#<math>
+\tau_2 = \tau (C_2) = \left\{ f_2 \mapsto \underline{C_2.f_2}, g_2 \mapsto \underline{C_2.g_2} \right\}
+</math>
+#<math>
+\mbox{dom} \left( \tau_2 \right) = \left\{ f_2, g_2 \right\}
+</math>
+And now the right part:
+#<math>
+\mbox {UNION} \ b \, \cdot \, \left(b \in \left\{ C_1 \right\}
        \ |\
-    \beta_{ S_{0} } \left( b \mapsto b \right) \ll \eta_{1, b}\right)
+    \mbox{ran}\left( \beta_{ S_{1} } \left( b \mapsto b \right) \ll \eta_{2, b} \right)\right)
+=
+\mbox{ran}\left( \beta_{ S_{1} } \left( C_1 \mapsto C_1 \right) \ll \eta_{2, C_1} \right)
+</math>
+#<math>
+   \beta_{ S_{1} } \left( C_1 \mapsto C_1 \right)
+=
+   \left\{ f_1 \mapsto f_1, g_1 \mapsto g_1\right\}
+</math>
+#<math>
+   \eta_{2,C_1} = \eta (C_2)(C_1) = \left\{ f_1 \mapsto f_2, g_1 \mapsto g_2 \right\}
+</math>
+#<math>
+   \left\{ f_1 \mapsto f_1, g_1 \mapsto g_1\right\} \ll \left\{ f_1 \mapsto f_2, g_1 \mapsto g_2 \right\}
+     =
+   \left\{ f_1 \mapsto f_2, g_1 \mapsto g_2 \right\}
+</math>
+#<math>
+   \mbox{ran}\left( \left\{ f_1 \mapsto f_2, g_1 \mapsto g_2\right\} \right)
+=
+   \left\{ f_2, g_2\right\}
+</math>
+So we get:
+<math>
+\beta_{S_2} \left( C_2 \mapsto C_2 \right)
+  =
+\left\{ f_2 \mapsto f_2, g_2 \mapsto g_2\right\}
+</math>
+====Calculate <math>\beta_{S_2} \left( C_1 \mapsto C_2 \right)</math>====
+According to the [[DynBindModel#The_naming_function|definition]]:
+<math>
+\beta_{S_2} \left( C_1 \mapsto C_2 \right)
+  =
+{\beta_{S_2}}^\prime \left( C_1 \mapsto C_2 \right)
+   \ll
+\theta_{S_2} \left( C_1 \mapsto C_2 \right)
+</math>
+Where:
+<math>
+{\beta_{S_2}}^\prime \left( C_1 \mapsto C_2 \right)
+  =
+\mbox {UNION} \ b \ \cdot \ \left(
+   b \in \alpha_2
+      \ |\
+   \beta_{S_{1}} \left( C_1 \mapsto b \right)
+      ;
+   \left(
+      \mbox{id} \left( \mbox{ran} \left( \beta_{S_{1}} \left( C_1 \mapsto b \right) \right) \right)
+         \ll
+      \eta_{2,b}
+   \right)
+\right)
+</math>
+And:
+<math>
+  \theta_{S_2} \left( C_1 \mapsto C_2 \right)
+    =
+  \mbox {UNION} \ b \ \cdot \ \left(
+   b \in \alpha_2
+      \ |\
+   \beta_{S_{1}} \left( C_1 \mapsto b \right)
+      ;
+   \left(
+      \mbox{id} \left( \mbox{ran} \left( \beta_{S_1} \left( C_1 \mapsto b \right) \right) \right)
+         \ll
+      \eta_{2,b}
+   \right)
+   \triangleright \sigma_{2,b}
+\right)
+</math>
+Here are the steps taken to compute the part:
+#<math>
+   \beta_{S_{1}} \left( C_1 \mapsto C_1 \right)
+      ;
+   \left(
+      \mbox{id} \left( \mbox{ran} \left( \beta_{S_{1}} \left( C_1 \mapsto C_1 \right) \right) \right)
+         \ll
+      \eta_{2,C_1}
+   \right)
+</math>
+##<math>
+  \mbox{id} \left( \mbox{ran} \left( \beta_{S_{1}} \left( C_1 \mapsto C_1 \right) \right) \right)
+    =
+  \left\{ f_1 \mapsto f_1, g_1 \mapsto g_1 \right\}
+</math>
+##<math>
+  \left\{ f_1 \mapsto f_1, g_1 \mapsto g_1 \right\} \ll \left\{ f_1 \mapsto f_2, g_1 \mapsto g_2 \right\}
+     =
+  \left\{ f_1 \mapsto f_2, g_1 \mapsto g_2 \right\}
+</math>
+##<math>
+  \left\{ f_1 \mapsto f_1, g_1 \mapsto g_1 \right\} \,;\, \left\{ f_1 \mapsto f_2, g_1 \mapsto g_2 \right\}
+    =
+  \left\{ f_1 \mapsto f_2, g_1 \mapsto g_2 \right\}
+</math>
+##<math>
+{\beta_{S_2}}^\prime \left( C_1 \mapsto C_2 \right)
+  =
+  \left\{ f_1 \mapsto f_2, g_1 \mapsto g_2 \right\}
+</math>
+#<math>
+   \beta_{S_1} \left( C_1 \mapsto C_1 \right)
+      ;
+   \left(
+      \mbox{id} \left( \mbox{ran} \left( \beta_{S_1} \left( C_1 \mapsto C_1 \right) \right) \right)
+         \ll
+      \eta_{2,C_1}
+   \right)
+   \triangleright \sigma_{2,C_1}
+</math>
+##<math>
+\sigma_{2,C_1} = \emptyset
+</math>
+##<math>
+  \mbox{id} \left( \mbox{ran} \left( \beta_{S_1} \left( C_1 \mapsto C_1 \right) \right) \right)
+    \ll
+  \emptyset
+     =
+  \emptyset
+</math>
+##<math>
+  \beta_{S_1} \left( C_1 \mapsto C_1 \right)
+      ;
+  \emptyset
+     =
+  \emptyset
+</math>
+##<math>
+  \theta_{S_2} \left( C_1 \mapsto C_2 \right) = \emptyset
+</math>
+# <math>
+  \left\{ f_1 \mapsto f_2, g_1 \mapsto g_2 \right\} \ll \emptyset
+    =
+  \left\{ f_1 \mapsto f_2, g_1 \mapsto g_2 \right\}
+</math>
+So we get:
+<math>
+\beta_{S_2} \left( C_1 \mapsto C_2 \right)
+  =
+\left\{ f_1 \mapsto f_2, g_1 \mapsto g_2 \right\}
+</math>
+====Putting the parts together:====
+We can know show the complete total function:
+{|border="0" cellpadding="2" cellspacing="0" align="center"
+|-valign="top" -halign="center"
+|
+<math>\beta_{S_2} = \{</math>
+|
+<math>
+   \left( C_1 \mapsto C_1 \right) \mapsto \left\{ f_1 \mapsto f_1, g_1 \mapsto g_1 \right\},
+</math>
+|-
+||
+|
+<math>
+   \left( C_1 \mapsto C_2 \right) \mapsto \left\{ f_1 \mapsto f_2, g_1 \mapsto g_2 \right\},
+</math>
+|-
+||
+|
+<math>
+   \left( C_2 \mapsto C_1 \right) \mapsto \emptyset,
+</math>
+|-
+||
+|
+<math>
+   \left( C_2 \mapsto C_2 \right) \mapsto \left\{ f_2 \mapsto f_2, g_2 \mapsto g_2 \right\} \ \}
+</math>
+|}
+===Calculating <math>\beta_{S_3}</math>===
+We will not show the complete construction of <math>\beta_{S_3}</math> but restrict our self to the most interesting parts.
+====Calculate <math>\beta_{S_3} \left( C_1 \mapsto C_3 \right)</math>====
+According to the [[DynBindModel#The_naming_function|definition]]:
+<math>
+\beta_{S_3} \left( C_1 \mapsto C_3 \right)
+  =
+{\beta_{S_3}}^\prime \left( C_1 \mapsto C_3 \right)
+   \ll
+\theta_{S_3} \left( C_1 \mapsto C_3 \right)
+</math>
+Where:
+<math>
+{\beta_{S_3}}^\prime \left( C_1 \mapsto C_3 \right)
+  =
+\mbox {UNION} \ b \ \cdot \ \left(
+   b \in \alpha_3
+      \ |\
+   \beta_{S_{2}} \left( C_1 \mapsto b \right)
+      ;
+   \left(
+      \mbox{id} \left( \mbox{ran} \left( \beta_{S_{2}} \left( C_1 \mapsto b \right) \right) \right)
+         \ll
+      \eta_{3,b}
+   \right)
+\right)
+</math>
+And:
+<math>
+\theta_{S_3} \left( C_1 \mapsto C_3 \right)
+   =
+\mbox {UNION} \ b \ \cdot \ \left(
+   b \in \alpha_3
+      \ |\
+   \beta_{S_{2}} \left( C_1 \mapsto b \right)
+      ;
+   \left(
+      \mbox{id} \left( \mbox{ran} \left( \beta_{S_{2}} \left( C_1 \mapsto b \right) \right) \right)
+         \ll
+      \eta_{3,b}
+   \right)
+   \triangleright \sigma_{3,b}
+\right)
+</math>
+Note that we can omit <math>\eta_{3,b}\,</math> from the formulas since it is always empty.
+#<math>
+   \beta_{S_2} \left( C_1 \mapsto C_2 \right)
+      ;
+   \mbox{id} \left( \mbox{ran} \left( \beta_{S_2} \left( C_1 \mapsto C_2 \right) \right) \right)
+   \ \cup \
+   \beta_{S_2} \left( C_1 \mapsto C_1 \right)
+      ;
+   \mbox{id} \left( \mbox{ran} \left( \beta_{S_2} \left( C_1 \mapsto C_1 \right) \right) \right)
+</math>
+##<math>
+   \beta_{S_{2}} \left( C_1 \mapsto C_2 \right)
+      =
+   \left\{ f_1 \mapsto f_2, g_1 \mapsto g_2 \right\}
+</math>
+##<math>
+  \mbox{id}\left(\mbox{ran}\left( \beta_{S_{2}} \left( C_1 \mapsto C_2 \right) \right)\right)
+     =
+  \left\{ f_2 \mapsto f_2, g_2 \mapsto g_2 \right\}
+</math>
+##<math>
+  \beta_{S_2} \left( C_1 \mapsto C_2 \right)
+    ;
+  \mbox{id} \left( \mbox{ran} \left( \beta_{S_2} \left( C_1 \mapsto C_2 \right) \right) \right)
+    =
+  \left\{ f_1 \mapsto f_2, g_1 \mapsto g_2 \right\}
+</math>
+##<math>
+   \beta_{S_{2}} \left( C_1 \mapsto C_1 \right)
+      =
+   \left\{ f_1 \mapsto f_1, g_1 \mapsto g_1 \right\}
+</math>
+##<math>
+  \mbox{id}\left(\mbox{ran}\left( \beta_{S_{2}} \left( C_1 \mapsto C_1 \right) \right)\right)
+     =
+  \left\{ f_1 \mapsto f_1, g_1 \mapsto g_1 \right\}
+</math>
+##<math>
+  \beta_{S_2} \left( C_1 \mapsto C_1 \right)
+    ;
+  \mbox{id} \left( \mbox{ran} \left( \beta_{S_2} \left( C_1 \mapsto C_1 \right) \right) \right)
+    =
+  \left\{ f_1 \mapsto f_1, g_1 \mapsto g_1 \right\}
+</math>
+##<math>
+  \left\{ f_1 \mapsto f_2, g_1 \mapsto g_2 \right\}
+  \ \cup\
+  \left\{ f_1 \mapsto f_1, g_1 \mapsto g_1 \right\}
+    =
+  \left\{ f_1 \mapsto f_1, f_1 \mapsto f_2, g_1 \mapsto g_1, g_1 \mapsto g_2 \right\}
+</math>
+#<math>
+   \beta_{S_2} \left( C_1 \mapsto C_2 \right)
+      ;
+   \mbox{id} \left( \mbox{ran} \left( \beta_{S_2} \left( C_1 \mapsto C_2 \right) \right) \right)
+      \ \triangleright\
+   \sigma_{3,C_2}
+   \ \cup \
+   \beta_{S_2} \left( C_1 \mapsto C_1 \right)
+      ;
+   \mbox{id} \left( \mbox{ran} \left( \beta_{S_2} \left( C_1 \mapsto C_1 \right) \right) \right)
+      \ \triangleright\
+   \sigma_{3,C_1}
+</math>
+##<math>
+   \sigma_{3,C_2} = \sigma \left(C_3 \right) \left(C_2\right) = \left\{ f_2 \right\}
+</math>
+##<math>
+   \sigma_{3,C_1} = \sigma \left(C_3 \right) \left(C_1\right) = \left\{ g_1 \right\}
 </math>
+##<math>
+   \beta_{S_2} \left( C_1 \mapsto C_2 \right)
+      ;
+   \mbox{id} \left( \mbox{ran} \left( \beta_{S_2} \left( C_1 \mapsto C_2 \right) \right) \right)
+      \ \triangleright\
+   \sigma_{3,C_2}
+      =
+   \left\{ f_1 \mapsto f_2 \right\}
+</math>
+##<math>
+   \beta_{S_2} \left( C_1 \mapsto C_1 \right)
+      ;
+   \mbox{id} \left( \mbox{ran} \left( \beta_{S_2} \left( C_1 \mapsto C_1 \right) \right) \right)
+      \ \triangleright\
+   \sigma_{3,C_1}
+      =
+   \left\{ g_1 \mapsto g_1 \right\}
+</math>
+##<math>
+   \left\{ f_1 \mapsto f_2 \right\} \ \cup \ \left\{ g_1 \mapsto g_1 \right\}
+      =
+   \left\{ f_1 \mapsto f_2, g_1 \mapsto g_1 \right\}
+</math>
+##<math>
+  \left\{ f_1 \mapsto f_1, f_1 \mapsto f_2, g_1 \mapsto g_1, g_1 \mapsto g_2 \right\}
+    \ll
+  \left\{ f_1 \mapsto f_2, g_1 \mapsto g_1 \right\}
+    =
+  \left\{ f_1 \mapsto f_2, g_1 \mapsto g_1 \right\}
+</math>
+So we get:
-We can forget about the right part of the union since <math>C_1\,</math> has no base classes. So we need to calculate:
+<math>
-<math>\mbox{id} \left( \mbox{dom} \left( \tau_1 \right) \right)</math>. To do so we give a little reminder on the identity and domain operators:
+\beta_{S_3} \left( C_1 \mapsto C_3 \right)
+  =
+  \left\{ f_1 \mapsto f_2, g_1 \mapsto g_1 \right\}
+</math>
+====The complete naming function====
+{|border="0" cellpadding="2" cellspacing="0" align="center"
+|-valign="top" -halign="center"
+|
+<math>\beta_{S_3} = \{</math>
+|
+<math>
+   \left( C_1 \mapsto C_1 \right) \mapsto \left\{ f_1 \mapsto f_1, g_1 \mapsto g_1 \right\},
+</math>
+|-
+||
+|
+<math>
+   \left( C_1 \mapsto C_2 \right) \mapsto \left\{ f_1 \mapsto f_2, g_1 \mapsto g_2 \right\},
+</math>
+|-
+||
+|
+<math>
+   \left( C_2 \mapsto C_1 \right) \mapsto \emptyset,
+</math>
+|-
+||
+|
+<math>
+   \left( C_2 \mapsto C_2 \right) \mapsto \left\{ f_2 \mapsto f_2, g_2 \mapsto g_2 \right\},
+</math>
+|-
+||
+|
+<math>
+   \left( C_1 \mapsto C_3 \right) \mapsto \left\{ f_1 \mapsto f_2, g_1 \mapsto g_1 \right\},
+</math>
+|-
+||
+|
+<math>
+   \left( C_2 \mapsto C_3 \right) \mapsto \left\{ f_2 \mapsto f_2, g_2 \mapsto g_2 \right\},
+</math>
+|-
+||
+|
+<math>
+   \left( C_3 \mapsto C_3 \right)
+      \mapsto
+   \left\{  f_1 \mapsto f_1, g_1 \mapsto g_1, f_2 \mapsto f_2, g_2 \mapsto g_2 \right\},
+</math>
+|-
+||
+|
+<math>
+   \left( C_3 \mapsto C_1 \right) \mapsto \emptyset,
+</math>
+|-
+||
+|
+<math>
+   \left( C_3 \mapsto C_2 \right) \mapsto \emptyset  \ \}
+</math>
+|}
+==The dynamic binding function==
+To calculate the dynamic binding function, we need to get <math>\delta_{S_3}</math>. We will again calculate it incrementally:
+===Calculating <math>\delta_{S_1}</math>===
+According to the [[DynBindModel#The_dynamic_binding_function|definition]]:
+<math>
+\delta_{S_1} \left( C_1 \mapsto C_1 \right)
+  =
+\beta_S \left( C_1 \mapsto C_1 \right) ;
+\left(
+\left( \mbox {UNION} \, b \cdot \left(
+    b \in \alpha_1
+      \, |\,
+    \left( \beta_S \left( b \mapsto b \right) ; \eta_{1,b} \right)^{-1}
+      ;
+    \delta_{S_0}\left( b \mapsto b \right)\right)  \right) \ll \tau_1
+\right)
+</math>
+Since <math>\alpha_1\,</math> is empty this simplifies to:
+<math>
+\delta_{S_1} \left( C_1 \mapsto C_1 \right)
+  =
+\beta_S \left( C_1 \mapsto C_1 \right) ; \tau_1
+  =
+\left\{ f_1 \mapsto f_1, g_1 \mapsto g_1 \right\}
+  ;
+\left\{ f_1 \mapsto \underline{C_1.f_1}, g_1 \mapsto \underline{C_1.g_1} \right\}
+</math>
+So we get:
+<math>
+\delta_{S_1}
+  =
+\left\{ \left( C_1 \mapsto C_1 \right) \mapsto
+   \left\{ f_1 \mapsto \underline{C_1.f_1}, g_1 \mapsto \underline{C_1.g_1} \right\}
+\right\}
+</math>
+===Calculating <math>\delta_{S_2}</math>===
+Again we calculate the different parts of the function in separate sections:
+====Calculate <math>\delta_{S_2}\left( C_1 \mapsto C_1 \right)</math>====
+According to the [[DynBindModel#The_dynamic_binding_function|definition]]:
 <math>
-    \mbox{id}\left( \left\{ e_1, \ldots, e_n \right\} \right)\ = \left\{ e_1 \mapsto e_1, \ldots, e_n \mapsto e_n \right\}
+    \delta_{S_2}\left( C_1 \mapsto C_1 \right) =
+   \delta_{S_1}\left( C_1 \mapsto C_1 \right) =
+      \left\{ f_1 \mapsto \underline{C_1.f_1}, g_1 \mapsto \underline{C_1.g_1} \right\}
 </math>
+====Calculate <math>\delta_{S_2}\left( C_2 \mapsto C_1 \right)</math>====
+According to the [[DynBindModel#The_dynamic_binding_function|definition]]:
 <math>
-    \mbox{dom}\left(\left\{ l_1 \mapsto r_1, \ldots, l_n \mapsto r_n \right\}\right) = \left\{ l_1, \ldots, l_n \right\}
+    \delta_{S_2}\left( C_1 \mapsto C_1 \right) = \emptyset
 </math>
-This done we calculate:
+====Calculate <math>\delta_{S_2}\left( C_2 \mapsto C_2 \right)</math>====
+According to the [[DynBindModel#The_dynamic_binding_function|definition]]:
+<math>
+  \delta_{S_2}\left( C_2 \mapsto C_2 \right)
+    =
+\beta_S \left( C_2 \mapsto C_2 \right) ;
+\left(
+\left( \mbox {UNION} \, b \cdot \left(
+    b \in \alpha_2
+      \, |\,
+    \left( \beta_S \left( b \mapsto b \right) ; \eta_{2,b} \right)^{-1}
+      ;
+    \delta_{S_1}\left( b \mapsto b \right)\right)  \right) \ll \tau_2
+\right)
+</math>
 #<math>
-\tau_1 = \tau (C_1) = \left\{ f_1 \mapsto \underline{C_1.f_1}, g_1 \mapsto \underline{C_1.g_1} \right\}
+  \mbox {UNION} \, b \cdot \left(b \in \left\{ C_1 \right\}
+      \, |\,
+    \left( \beta_S \left( b \mapsto b \right) ; \eta_{2,b} \right)^{-1}
+      ;
+    \delta_{S_1}\left( b \mapsto b \right)\right)
+    =
+    \left( \beta_S \left( C_1 \mapsto C_1 \right) ; \eta_{2,C_1} \right)^{-1}
+      ;
+    \delta_{S_1}\left( C_1 \mapsto C_1 \right)
+</math>
+##<math>
+  \beta_S \left( C_1 \mapsto C_1 \right) ; \eta_{2,C_1}
+    =
+  \left\{ f_1 \mapsto f_2, g_1 \mapsto g_2 \right\}
+</math>
+##<math>
+  \left( \beta_S \left( C_1 \mapsto C_1 \right) ; \eta_{2,C_1} \right)^{-1}
+    =
+  \left\{ f_2 \mapsto f_1, g_2 \mapsto g_1 \right\}
+</math>
+##<math>
+  \left( \beta_S \left( C_1 \mapsto C_1 \right) ; \eta_{2,C_1} \right)^{-1}
+      ;
+   \delta_{S_1}\left( C_1 \mapsto C_1 \right)
+    =
+ \left\{ f_2 \mapsto \underline{C_1.f_1}, g_2 \mapsto \underline{C_1.g_1} \right\}
 </math>
 #<math>
-\mbox{dom} \left( \tau_1 \right) = \left\{ f_1, g_1 \right\}
+  \tau_2 = \tau \left( C_2 \right)
+    =
+  \left\{ f_2 \mapsto \underline{C_2.f_2}, g_2 \mapsto \underline{C_2.g_2} \right\}
 </math>
 #<math>
-\mbox{id} \left( \mbox{dom} \left( \tau_1 \right) \right) = \left\{ f_1 \mapsto f_1, g_1 \mapsto g_1\right\}
+  \left\{ f_2 \mapsto \underline{C_1.f_1}, g_2 \mapsto \underline{C_1.g_1} \right\}
+    \ll
+  \left\{ f_2 \mapsto \underline{C_2.f_2}, g_2 \mapsto \underline{C_2.g_2} \right\}
+    =
+  \left\{ f_2 \mapsto \underline{C_2.f_2}, g_2 \mapsto \underline{C_2.g_2} \right\}
 </math>
 So we get:
+<math>
+  \delta_{S_2}\left( C_2 \mapsto C_2 \right)
+    =
+  \left\{ f_2 \mapsto \underline{C_2.f_2}, g_2 \mapsto \underline{C_2.g_2} \right\}
+</math>
+====Calculate <math>\delta_{S_2}\left( C_1 \mapsto C_2 \right)</math>====
+According to the [[DynBindModel#The_dynamic_binding_function|definition]]:
+<math>
+  \delta_{S_2}\left( C_1 \mapsto C_2 \right)
+    =
+\beta_S \left( C_1 \mapsto C_2 \right) ;
+\left(
+\left( \mbox {UNION} \, b \cdot \left(
+    b \in \alpha_2
+      \, |\,
+    \left( \beta_S \left( b \mapsto b \right) ; \eta_{2,b} \right)^{-1}
+      ;
+    \delta_{S_{1}}\left( b \mapsto b \right)\right)  \right) \ll \tau_{2}
+\right)
+</math>
+At this stage it should be clear how to calculate this, so we just give the result:
+<math>
+  \delta_{S_2}\left( C_1 \mapsto C_2 \right)
+    =
+  \left\{ f_1 \mapsto \underline{C_2.f_2}, g_1 \mapsto \underline{C_2.g_2} \right\}
+</math>
+====Putting the parts together:====
+We can know show the complete total function:
+{|border="0" cellpadding="2" cellspacing="0" align="center"
+|-valign="top" -halign="center"
+|
+<math>\delta_{S_2} = \{</math>
+|
+<math>
+   \left( C_1 \mapsto C_1 \right)
+      \mapsto
+   \left\{ f_1 \mapsto \underline{C_1.f_1}, g_1 \mapsto \underline{C_1.g_1} \right\},
+</math>
+|-
+||
+|
+<math>
+   \left( C_1 \mapsto C_2 \right)
+      \mapsto
+   \left\{ f_1 \mapsto \underline{C_2.f_2}, g_1 \mapsto \underline{C_2.g_2} \right\},
+</math>
+|-
+||
+|
+<math>
+   \left( C_2 \mapsto C_1 \right) \mapsto \emptyset,
+</math>
+|-
+||
+|
+<math>
+   \left( C_2 \mapsto C_2 \right)
+      \mapsto
+    \left\{ f_2 \mapsto \underline{C_2.f_2}, g_2 \mapsto \underline{C_2.g_2} \right\} \ \}
+</math>
+|}
+===Calculating <math>\delta_{S_3}</math>===
+There is nothing new for this calculation so we just present the result:
+{|border="0" cellpadding="2" cellspacing="0" align="center"
+|-valign="top" -halign="center"
+|
+<math>\delta_{S_3} = \{</math>
+|
+<math>
+   \left( C_1 \mapsto C_1 \right)
+      \mapsto
+   \left\{ f_1 \mapsto \underline{C_1.f_1}, g_1 \mapsto \underline{C_1.g_1} \right\},
+</math>
+|-
+||
+|
+<math>
+   \left( C_1 \mapsto C_2 \right)
+      \mapsto
+   \left\{ f_1 \mapsto \underline{C_2.f_2}, g_1 \mapsto \underline{C_2.g_2} \right\},
+</math>
+|-
+||
+|
+<math>
+   \left( C_2 \mapsto C_1 \right) \mapsto \emptyset,
+</math>
+|-
+||
+|
+<math>
+   \left( C_2 \mapsto C_2 \right)
+      \mapsto
+    \left\{ f_2 \mapsto \underline{C_2.f_2}, g_2 \mapsto \underline{C_2.g_2} \right\},
+</math>
+|-
+||
+|
+<math>
+  \left( C_1 \mapsto C_3 \right)
+    \mapsto
+  \left\{ f_1 \mapsto \underline{C_2.f_2}, g_1 \mapsto \underline{C_3.g_1} \right\},
+</math>
+|-
+||
+|
 <math>
-    \beta_{S_1}\left( C_1 \mapsto C_1 \right) = \left\{ f_1 \mapsto f_1, g_1 \mapsto g_1\right\}
+  \left( C_2 \mapsto C_3 \right)
+    \mapsto
+  \left\{ f_2 \mapsto \underline{C_2.f_2}, g_2 \mapsto \underline{C_2.g_2} \right\},
+</math>
+|-
+||
+|
+<math>
+   \left( C_3 \mapsto C_3 \right)
+      \mapsto
+    \left\{ f_1 \mapsto \underline{C_3.f_1}, g_1 \mapsto \underline{C_3.g_1},
+           f_2 \mapsto \underline{C_2.f_2}, g_2 \mapsto \underline{C_2.g_2} \right\},
+</math>
+|-
+||
+|
+<math>
+   \left( C_3 \mapsto C_1 \right) \mapsto \emptyset,
+</math>
+|-
+||
+|
+<math>
+   \left( C_3 \mapsto C_2 \right) \mapsto \emptyset  \ \}
+</math>
+|}
+===Deriving the dynamic binding function===
+The function is now given. We evaluate it at two interesting points:
+*<math>
+  \delta\left( C_1 \mapsto f_1 \right)
+    =
+  \left\{
+    C_1 \mapsto \underline{C_1.f_1}, C_2 \mapsto \underline{C_2.f_2}, C_3 \mapsto \underline{C_2.f_2}
+  \right\}
 </math>
-===Calculating <math>\beta_{S_2}</math>===
+*<math>
+  \delta\left( C_1 \mapsto f_g \right)
+    =
+  \left\{
+    C_1 \mapsto \underline{C_1.f_g}, C_2 \mapsto \underline{C_2.g_2}, C_3 \mapsto \underline{C_2.g_1}
+  \right\}
+</math>

DynBindModelExamples: Difference between revisions

Latest revision as of 10:11, 11 April 2007

The system

The naming function

Calculating βS1

Calculating βS2

Calculate βS2(C1↦C1)

Calculate βS2(C2↦C1)

Calculate βS2(C2↦C2)

Calculate βS2(C1↦C2)

Putting the parts together:

Calculating βS3

Calculate βS3(C1↦C3)

The complete naming function

The dynamic binding function

Calculating δS1

Calculating δS2

Calculate δS2(C1↦C1)

Calculate δS2(C2↦C1)

Calculate δS2(C2↦C2)

Calculate δS2(C1↦C2)

Putting the parts together:

Calculating δS3

Deriving the dynamic binding function

Navigation menu

Search

Calculating $β_{S_{1}}$

Calculating $β_{S_{2}}$

Calculate $β_{S_{2}} (C_{1} \mapsto C_{1})$

Calculate $β_{S_{2}} (C_{2} \mapsto C_{1})$

Calculate $β_{S_{2}} (C_{2} \mapsto C_{2})$

Calculate $β_{S_{2}} (C_{1} \mapsto C_{2})$

Calculating $β_{S_{3}}$

Calculate $β_{S_{3}} (C_{1} \mapsto C_{3})$

Calculating $δ_{S_{1}}$

Calculating $δ_{S_{2}}$

Calculate $δ_{S_{2}} (C_{1} \mapsto C_{1})$

Calculate $δ_{S_{2}} (C_{2} \mapsto C_{1})$

Calculate $δ_{S_{2}} (C_{2} \mapsto C_{2})$

Calculate $δ_{S_{2}} (C_{1} \mapsto C_{2})$

Calculating $δ_{S_{3}}$