Example 2 As an example of an (informal) derivation in this calculus, we
show that
Γ, {Fι}X{F2} 'h {F1}P{F2}
Γ 'h {F1}μX(P){F2}
is a derived rule:
(μ)
1. 'h {F1}fail{F1 ∧ false}
2. 'h {F1}fail{F2}
3. Γ 'H {F1}fail{F2}
4. Γ, {F1}X{F2} 'H {F1}P{F2}
5. Γ 'h {F1}hX ^ Pi(X){F2}
(Test)
(Consequence, 1)
(Weakening, 2)
(premise)
(Recursion, 3,4)
Example 3 A second example uses the rule we have just derived to show
that
Γ '{F ∧ B}P{F}
Γ '{F}while B do P od {F ∧-B}
(while)
is another derived rule.
1.
Γ 'H {F ∧ B}P{F}
(premise)
2.
'H {F}B?{F ∧ B}
(Test)
3.
Γ 'H {F}B?; P{F}
(Composition, 1,2)
4.
{F}X{F ∧ -B} 'H {F}X{F ∧ -B}
(Id)
5.
Γ, {F}X{F ∧ -B} 'H {F}B?; P; X{F ∧ -B}
(Composition, 3,4)
6.
'h {F}-B?{F ∧-B}
(Test)
7.
Γ, {F}X{F ∧ -B} 'h {F}(B?; P; X) ∪ -B?{F ∧ -B} (Choice, 5,6)
8.
Γ 'h {F}μX((B?; P; X) ∪ -B?){F ∧ -B}
(μ, 7)
We can give a rather straightforward proof of the soundness of the calculus
H by simply considering the translations of its axioms and rules. For any set
of asserted programs Γ, we write Γ for the set of translations {Ct | C ∈ Γ}.
25
More intriguing information
1. Should informal sector be subsidised?2. SOCIOECONOMIC TRENDS CHANGING RURAL AMERICA
3. The name is absent
4. The name is absent
5. Multimedia as a Cognitive Tool
6. Herman Melville and the Problem of Evil
7. Behavioural Characteristics and Financial Distress
8. The name is absent
9. The name is absent
10. The name is absent