Plt1213 3

(C) Ralf Lämmel, Andrei Varanovich, University of Koblenz Landau

Logistics

Assignment

1. Inspired by Lemma 2.19 from the lecture on semantics-based reasoning, let's do an experiment on instrumenting the semantics (i.e., the Prolog-based interpreter) to play with the intuition behind the lemma. That is, let's instrument the SOS implementation so that it counts the number derivation steps performed. Let us then invoke the semantics to count steps for a non-completely trivial statement sequence. Let us compare the count with the (sum of the) counts for invoking the semantics instead on the two constituents of the sequence individually.

2. Determine the height of the derivation tree for the factorial sample program, when using the natural semantics. To this end, instrument the semantics (i.e., the Prolog-based interpreter) to compute the height of the derivation tree. Let's agree on counting the height of derivation trees for axioms as 0 and the height of rules with premises is the maximum height for the premises plus 1.