MCS-287 Homework 8 (Spring 2009)

Due May 12, 2009

• Do exercise 21.1 on page 472. Don't worry about cases where the given `riddle` predicate would go into infinite loops: your more efficient predicate can do something different in those cases.

• Do exercise 21.2 on page 472.

• Exercise 23.x1: Using the natural semantics for Language One, show how the conclusion `plus(const(2),times(const(3),const(4)))`→14 would be derived. That is, what are the immediately preceding premises from which a rule allows this conclusion to be derived? And for any of those immediately preceding premises that is itself a consequence of applying some rule to earlier premises, what are those? (You can structure this as a tree, as demonstrated in class.)

• Exercise 23.x2: Using the natural semantics for Language Two, show how the conclusion ⟨`let(x,const(2),times(var(x),const(4)))`, [ ]⟩→8 would be derived. That is, what are the immediately preceding premises from which a rule allows this conclusion to be derived? And for any of those immediately preceding premises that is itself a consequence of applying some rule to earlier premises, what are those? (You can structure this as a tree, as demonstrated in class.)

• Exercise 23.x3: The natural semantics rules for Language Two make use of an auxilliary function lookup. This can be eliminated if two different rules are used for `var` expressions. One of these rules is ⟨`var(`x`)`, bind(x,v)::C⟩→v. What is the other rule? Hint 1: Look at the Prolog rules for the `lookup` predicate. Hint 2: In addition to the premises listed above the line in a natural semantics rule, you can also have a "side condition" listed next to the rule. This is any mathematical condition on the rule's metavariables that must hold in order for the rule to be applicable. For example, the rule for `plus` could be rewritten with v3 in the conclusion in place of v1+v2, provided that a side condition is written next to the rule, namely v3=v1+v2. (In this case, the version with the side condition would be less elegant.)