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

Sale!