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. Recognizability of Individual Creative Style Within and Across Domains: Preliminary Studies2. The name is absent
3. Strategic Policy Options to Improve Irrigation Water Allocation Efficiency: Analysis on Egypt and Morocco
4. Importing Feminist Criticism
5. Ein pragmatisierter Kalkul des naturlichen Schlieβens nebst Metatheorie
6. CONSUMER PERCEPTION ON ALTERNATIVE POULTRY
7. An Efficient Secure Multimodal Biometric Fusion Using Palmprint and Face Image
8. The name is absent
9. Peer Reviewed, Open Access, Free
10. GENE EXPRESSION AND ITS DISCONTENTS Developmental disorders as dysfunctions of epigenetic cognition