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. The Economics of Uncovered Interest Parity Condition for Emerging Markets: A Survey2. The growing importance of risk in financial regulation
3. How Low Business Tax Rates Attract Multinational Headquarters: Municipality-Level Evidence from Germany
4. Evaluation of the Development Potential of Russian Cities
5. Permanent and Transitory Policy Shocks in an Empirical Macro Model with Asymmetric Information
6. The name is absent
7. Education and Development: The Issues and the Evidence
8. Stillbirth in a Tertiary Care Referral Hospital in North Bengal - A Review of Causes, Risk Factors and Prevention Strategies
9. Three Strikes and You.re Out: Reply to Cooper and Willis
10. Migrant Business Networks and FDI