Corollary 14 (Scott’s Induction Rule) Assume X1, . . . , Xn are not free
in C. Write C(Q) for [Q/X]C. Then
C ([fail/Xi,..., fail∕Xn]P )+
∀X111.Xn(C(P)^→C∖[Pι∕Xι,11.,Pn∕Xn]Pr AX
C(hXi ^ Pi)i(P))+
8 Hoare’s Calculus
As a simple application we show that our semantics subsumes the Hoare
Calculus, which we shall present in Gentzen form. Sequents Γ 'h C will
consist of a set of asserted programs Γ and an asserted program C. The
derivability relation 'PA between assertions F is given by an axiomatization
of first-order logic plus the first-order Peano axioms. Structural rules of our
Hoare-Gentzen calculus are the following.
C 'h C
Γι 'h C
Γι, Γ2 'h C
Γι 'h Ci Γ2,C1 'h C2
γ1, γ2 'h C2
(Id)
(Weakening)
(Cut)
The following logical rules embody the Hoare Calculus.
'H {[N∕x]F}x := N{F}
(Assignment)
'H {F}B?{F ∧ B} (Test)
Γi 'h {F1}P1{F2} Γ2 'h {F2}P2{F3}
Γι, Γ2 'h {Fi}Pi; P2{F3}
Γι 'h {F1}P1{F2} Γ2 'h {F1}P2{F2}
Γι, Γ2 'h {F1}P1 ∪ P2{F2}
Γ 'H {F1}[fail∕X1,..., fail∕Xn]P {F2}
Γ, {Fι}P{F2} 'h {F1}[P1∕X1,..., Pn/Xn]P{F2}
Γ 'h {F}lXi ^ Pi)n,l(P){F2}
(Composition)
(Choice)
(Recursion)
Fi 'PA F2 Γ 'h {F2}P{F3} F3 'PA F4
Γ 'h {Fi}P{F4}
(Consequence)
24
More intriguing information
1. ISO 9000 -- A MARKETING TOOL FOR U.S. AGRIBUSINESS2. 101 Proposals to reform the Stability and Growth Pact. Why so many? A Survey
3. The name is absent
4. Imputing Dairy Producers' Quota Discount Rate Using the Individual Export Milk Program in Quebec
5. PROPOSED IMMIGRATION POLICY REFORM & FARM LABOR MARKET OUTCOMES
6. On the estimation of hospital cost: the approach
7. 09-01 "Resources, Rules and International Political Economy: The Politics of Development in the WTO"
8. The name is absent
9. DETERMINANTS OF FOOD AWAY FROM HOME AMONG AFRICAN-AMERICANS
10. Inhimillinen pääoma ja palkat Suomessa: Paluu perusmalliin