Program Semantics and Classical Logic



skip
fail


if B then P1 else P2 fi
μX (P)


while B do P od


is short for
is short for
is short for
is short for
is short for


true?

false


(B?; Pi) (-B?; P2)
hX ^ P i(X)

μX((B?; P; X) -B?)


Remark on notation. The sequence operator “;” is associative, both on its
intuitive interpretation (P
i; P2 meaning “do Pi and then P2”) and given the
semantics (relational composition) it gets in this paper and elsewhere. We
shall also make no
syntactic distinction between (Pi; P2); P3 and Pi; (P2; P3)
and write both as P
i ; P2; P3. Similarly, we syntactically identify P with
skip; P and with P;skip. This is allowed because skip intuitively means
“do nothing” and will be interpreted formally as the
diagonal relation {hi, ii |
i is a state}. The identification will allow us to say that the programs Pi ; P
and P; P
2 , as well as the program P, have the form Pi ; P; P2: we can take
P
i or P2 or both to be the identity element skip.

An occurrence of a program variable Y {Xi , . . . , Xn} is free in a program
P if it does not occur within a subprogram of the form hXi ^ Piin=1(P0) in
P . A program is
closed if it contains no free program variables.

Our procedure declarations can bind a series of program variables simul-
taneously, and since procedure declarations may make mutual calls it will not
be possible to reduce this form of binding to an
iteration of bindings, as it
can usually be done in logic. Since we shall also have occasion to work with
simultaneous substitutions, things threaten to get a bit complicated. The
following definition may look a bit hairy, but in fact gives a straightforward
generalisation of the usual notion of substitution.

Definition 3 (Substitution) The simultaneous substitution [Pi/Xi]in=1P
of P
1 for X1 and . . . and Pn for Xn in P (abbreviated as [Pi/Xi]iP) is defined
as follows.

[Pi/Xi]iXk = Pk, if 1 kn

[Pi/Xi]iA = A, ifA/ {X1,...,Xn}

[Pi/Xi]i(Q1; Q2) = [Pi/Xi]i Q1; [Pi/Xi]iQ2

[Pi∕Xi]i(Qι Q2) = [Pt∕Xi]i Qi [Pi∕Xi]i Q2



More intriguing information

1. The name is absent
2. Return Predictability and Stock Market Crashes in a Simple Rational Expectations Model
3. Evaluating Consumer Usage of Nutritional Labeling: The Influence of Socio-Economic Characteristics
4. A MARKOVIAN APPROXIMATED SOLUTION TO A PORTFOLIO MANAGEMENT PROBLEM
5. CONSUMER ACCEPTANCE OF GENETICALLY MODIFIED FOODS
6. The name is absent
7. Altruism with Social Roots: An Emerging Literature
8. How to do things without words: Infants, utterance-activity and distributed cognition.
9. Firm Creation, Firm Evolution and Clusters in Chile’s Dynamic Wine Sector: Evidence from the Colchagua and Casablanca Regions
10. An Estimated DSGE Model of the Indian Economy.
11. Rent-Seeking in Noxious Weed Regulations: Evidence from US States
12. The name is absent
13. Does Presenting Patients’ BMI Increase Documentation of Obesity?
14. The name is absent
15. Deletion of a mycobacterial gene encoding a reductase leads to an altered cell wall containing β-oxo-mycolic acid analogues, and the accumulation of long-chain ketones related to mycolic acids
16. Group cooperation, inclusion and disaffected pupils: some responses to informal learning in the music classroom
17. Locke's theory of perception
18. Psychological Aspects of Market Crashes
19. The name is absent
20. AGRIBUSINESS EXECUTIVE EDUCATION AND KNOWLEDGE EXCHANGE: NEW MECHANISMS OF KNOWLEDGE MANAGEMENT INVOLVING THE UNIVERSITY, PRIVATE FIRM STAKEHOLDERS AND PUBLIC SECTOR