Combining our findings, we conclude that
Rm+1 ⊆ [{V(Lt,α) I ∃L0 : L 'C [hXi ^ PK,ι(Pj)∕X,]‰1L⅛L0 'C Pk}
Since, by Lemma 20, L0 'C Pk implies that
[(Xi ^ Piin=I(Pj)/XjL 'C [(Xi ^ Piin=ι(Pj)∕X]n=ιPk
It follows that
R ' ⊆ [{V(Lt,α) I L 'C [(Xi ^ Pi)i=ι(P,)∕Xi]J=ιPk}
⊆ [{V(Lt, a) I L 'C (Xi ^ Piii=ι(Pk)}
We may conclude that Sm Rk' ⊆ S{V(Lt, a) ∣ L 'C (Xi ^ Pii*=1(P⅛)} for all
k and now reason as follows.
V(((Xi ^ Piin=ι(Pk))t,α) = (Lemma 8)
V (Pkt,α[Rω/Xι,...,Rω /Xn]) = (continuity)
[V(Pkt,a[R1m/X1,...,Rnm/Xn])=[Rkm ⊆
mm
[{V(Lt,a) I L 'C (Xi ^ Pi)i=ι(Pk)}
This concludes the proof. □
10 Conclusion and Further Prospects
In this paper we have shown that at least some non-trivial programming
constructs, including recursion, can be provided with a semantics in the
models of ordinary second-order logic, using the technique of translating
programs and correctness statements into that logic as it is commonly done
in Montague Semantics. The programming language which we have treated
was very small of course, but there seem to be no reasons why we should
not be able in principle to extend it with many useful constructs. This is
one way to continue from here, but there are other possibilities as well. We
speculate on two of them.
• In this paper we have only looked at an imperative language, but the
procedural semantics of logic programming languages is usually done in
the denotational framework as well and makes extensive use of fixpoint
constructions. The idea that we could have a logical treatment of the
procedural semantics of these languages is tantalising.
30
More intriguing information
1. The name is absent2. Palvelujen vienti ja kansainvälistyminen
3. Improving behaviour classification consistency: a technique from biological taxonomy
4. Valuing Farm Financial Information
5. AN ECONOMIC EVALUATION OF THE COLORADO RIVER BASIN SALINITY CONTROL PROGRAM
6. EDUCATIONAL ACTIVITIES IN TENNESSEE ON WATER USE AND CONTROL - AGRICULTURAL PHASES
7. ¿Por qué se privatizan servicios en los municipios (pequeños)? Evidencia empírica sobre residuos sólidos y agua.
8. The mental map of Dutch entrepreneurs. Changes in the subjective rating of locations in the Netherlands, 1983-1993-2003
9. Tourism in Rural Areas and Regional Development Planning
10. The name is absent