HW 5 COSC 4780

HW 5
COSC 4780
Assignment:
1. Read pages 1 – 14 of the Schmidt text.
2. Using the style of proof presented in the notes below, prove that the
example in figure 1.5 (pp. 10) is well-typed.
3. Prove the following commands are (or are not) well-typed.
loc1 := 0; while ¬(@loc1 = 0) do loc1 := @loc2 + 1 od : comm
@loc1 := 0
loc1 := @loc1 = 0
1 The Core Language
We are using the core language from Schmidt.
1.1 Syntax
The syntax for the core language is
C ::= L:=E | C1; C2 | if E then C1 else C2 fi | while E do C od | skip
E ::= N | @L | E1 + E2 | ¬E | E1 = E2
L ::= loci
if i > 0
N ::= n if n ∈ Z
1.2 Types
The types are int, intloc, intexp, boolexp and comm.
1.3 Typing Rules
The typing rules can be sued to build derivations showing a syntactically wellformed phrase is well-typed. There are four styles of rules here.
For the purposes of the following discussion, let P, P1, P2, P3 ∈ {C, E, L, N}
be meta-variables denoting syntactic classes and let T, T1, T2, T3 ∈ {int, intloc, intexp, boolexp, comm}
be meta-variables denoting types.
Rules of the following form are axiom rules.
P :T
if C
They may (or may not) have a side condition C, which if it holds, means there
is nothing more to prove.
Rules of the form
P1 :T1
P :T
P1 :T1 P2 :T2
P :T
P1 :T1 P2 :T2 P3 :T3
P : T
1
These rules have hypotheses which are typing goals that remain to be shown.
Rules used here have one, two or three hypotheses.
The typing rules for the core languages are as follows:
For Location: For Numeral
loci
: intloc if i > 0 N : int if n ∈ Z
For Expression:
N : int
N : intexp
L : intloc
@L : intexp
E1 : intexp E2 : intexp
E1 + E2 : intexp
E : boolexp
¬E : boolexp
E1 : τexp E2 : τexp
E1 = E2 : boolexp if τ ∈ {int, bool}
For Command:
L : intloc E : intexp
L:=E : comm
C1 : comm C2 : comm
C1 ; C2: comm skip : comm
E : boolexp C1 : comm C2 : comm
if E then C1 else C2 fi : comm
E : boolexp C : comm
while E do C od : comm
1.4 Building type derivations
My style of writing typing derivations differs a bit from Schmidt’s. You can see
examples of his style in figure 1.3 on page 4. The following examples will show
how I do it.
Example 1.1. As a first example, I present a derivation that the phrase loc1 :=
5 + @loc2 is a well-typed command. Thus, the goal is to build a derivation
justifying the following typing assertion.
loc1 := 5 + @loc2 : comm
Find a rule that matches by considering the syntax of the phrase and the
type and matching against the bottom line of a typing rules. In this case, the
assignment rule matches with a substitution of the following form:
{L := loc1, E := 5 + @loc1}
The way to see that this works is to apply the substitution to the goal of the
typing rule and notice that the result is exactly the goal we are trying to show.
Note that, for example, the additition rules does not match this goal – there is
no substitution that can be applied to the goal of that rule E1 + E2 : intexp
that will yield the assertion we are trying to show. To build the subgoals we
must derive, replace L in the left hypotheses of the rule by loc1 and replace E
in the right hypothesis by the expression 5 + @loc2. This yields the following
partial derivation.
2
@loc1 : intloc 5 + @loc2 : intexp
loc1 := 5 + @loc2 : comm
Now, on the left branch, since 1 > 0 we know the loc1 is well-typed. This closes
the left branch.
loc1 : intloc 5 + @loc2 : intexp
loc1 := 5 + @loc2 : comm
On the right side, the rule for typing int-expressions defined by addition applies
using the following match.
{E1 := 5, E2 := @loc2
Apply the rule by writing down a line ober the open subgoal and writing down
the result of applying the matching substitution to the two subgoals E1 : intexp
and E2 : intexp above the line. This yields the following partial derivation.
loc1 : intloc
5 : intexp @loc2 : intexp
5 + @loc2 : intexp
loc1 := 5 + @loc2 : comm
On the leftmost open branch, the rule for showing a numeral is an int-expression
applies and then the axiom rule for numerals as int holds because the side
condition holds i.e. that 5 is an integer. Applying these two rules to the left
open branch yields the following.
loc1 : intloc
5 : int
5 : intexp @loc2 : intexp
5 + @loc2 : intexp
loc1 := 5 + @loc2 : comm
For the right open branch, we match the rule for typing the dereference operator.
This rule says, to show that an assertion of the form @L : intexp holds, show
that the assertion L : intloc. There is an axiom rule for assertions of this form.
In this case, L is loc2 and 2 > 0 so so the side condition holds. Applying both
rules apply closes the open branch of the derivation yielding a completed type
derivation.
loc1 : intloc
5 : int
5 : intexp
loc2 : intloc
@loc2 : intexp
5 + @loc2 : intexp
loc1 := 5 + @loc2 : comm
3
Example 1.2. Here’s a derivation that the command
if @loc1 = 0 then loc1 := @loc2 else skip fi
is a well-typed command i.e. that it has type comm.
loc1 : intloc
@loc1 : intexp
0 : int
0 : intexp
@loc1 = 0 : boolexp
loc1 : intloc
loc2 : intloc
@loc2 : intexp
loc1 := @loc2 : comm skip : comm
if @loc1 = 0 then loc1 := @loc2 else skip fi: comm
4