Due date: 10/26 @ at the beginning of class
The goal of this problem set is to understand the role of types and type
checking. In addition, you will demonstrate that you can expand your
knowledge of a computing system (Redex) on your own
The following revision of simple-lang equips the language with
Here are the examples from the last problem set, adjusted to this new
;; specifying syntax
(st (x = et) (block (dt ...) st ...))
(et x n (+ et et) (coerce t et))
(dt (t x n))
(t int float)
Use this code to create your solution file.
(term (block ((int x 0) (int y 1)) (x = (+ x 1)) (y = x))))
(block ((int x 8) (int y 9))
(x = 0)
(block ((int z 9))
(x = 0)
(z = 2))
(y = 1))))
(term (block ((int x 0)) (block ((int x 9)) (x = (+ x 1))))))
(term (block ((int x 0)) (block ((int y 9)) (block ((int z 3)) (y = x))))))
(term (block ((int x 0)) (x = 1) (x = (+ x 1)))))
(for/and ((an-s (list s3 s1 s4 s2)))
(redex-match? simple-lang st an-s))
Design the type judgment check, which consumes a statement
st and checks whether st satisfies the type
constraints. In particular, check enforces the following
These rules correspond to those of Algol, C, and Java except that these
languages automatically convert int-typed expressions to
float-typed expressions. In simple-lang, you need an
explicit coerce expression to convert a value from one type to
in the ith declaration of a block, the declared type is equal to
the type of the initial value;
each statement inside of a block satisfies the type constraints;
the declared type of the left-hand side of an assignment is
equal to the type of the right-hand side;
similarly, the type of a variable is the specified type of the closest
matching variable declaration;
the type of a number is int if it is a
and float if it is an flonum?
the types of the two subexpression of an addition expression are equal
and the type of the addition expression is the same as the type of its two
Warning The side-condition of judgments differs
from those of reduction rules and meta functions.
Once the type checker has checked the constraints for a statement
st, it is possible to strip all type-related information from
st to determine its behavior via the standard reduction
Copy and paste the relevant pieces of your standard reduction relation
from problem set 6 into your solution file. Correct any mistakes that were
Design the function strip, which consumes a statement st
and strips all type-related elements.
Design the function eval-st, which consumes a statement and
determines its behavior according to the untyped reduction semantics. For
the latter step, it strips all type-related elements. If a statement does
not type check, the function produces error.
Hint I have carefully engineered the above language
definition so that copy-and-paste should work without problem. --
In principle, a semantics engineer would organize such a model in several
files and import the untyped reduction relation.
Implementations for languages such as Algol have used type information to
compile and run code. Stripping type information was common for languages
such as SML; for example, the SML/NJ implementation used to translate its
input to Scheme.
Claim: All programs (typed or untyped) in simple-lang terminate.
Articulate the central proof idea in 20 words or less.
Design the function size, which
the size of statements s in the
untyped simple-lang language.
Hint You may wish to turn your proof into an executable
metafunction that traces the standard reductions of
simple-lang programs and confirms your conjecture. Doing so
requires some learning about traces and a modicum of Racket
knowledge. Follow this hint only if you have time.
Send in a single Racket file. Its name should
consist of the two last names in alphabetical order separated with a
hyphen; its suffix must be .rkt.
Your file must start with the following two lines:
appropriately instantiated of course. Also separate problems with lines of
the shape ";; " followed by 77 "-". That gives you a width of 80 chars. Try
to stick to this width for all of your code; it ensures basic readability.
;; NameOfPartner1, NameOfPartner2
;; firstname.lastname@example.org, email@example.com