Homework #12 Questions

Small-Step-Semantics

Q: Can you give me an example of running small-step semantics on an apply node?

A: Sure: 

?- step(apply(fn(x,plus(const(2),var(x))),const(4)),X).

X = plus(const(2), const(4)) 

Yes

Q: What does e2[x → v1] mean ?

A: It means substitute var(x) with v1 wherever it occurs in e2

Q: Can you give an example of subst in action?

A: OK 

?- subst(plus(var(x),var(y)),x,times(var(y),const(4)),X).

X = plus(times(var(y), const(4)), var(y)) 

Yes

Q: How does small-step semantics work?

A: Sorry I didn't get to this in class. Here's an example: 

(1+2)+(3+4) -> 3+(3+4) -> 3 + 7 -> 10
Here's the proof of the first step: 
   
   --------- (rule 3 with n1 = "1", n2 = "2")
   1+2 -> 3
--------------------- (rule 1 with e1 = "1+2", e2 = "3+4", e1' = "3")
(1+2)+(3+4) -> 3+(3+4)
Notice how rule 3 uses typewriter font ``+'' to mean a syntactic plus in the program, and uses a mathematical ``+'' to mean actual addition.

The first step in AST (prolog) terms, is proved by the following predicate: 

?- step(plus(plus(const(1),const(2)),plus(const(3),const(4))),
        plus(const(3),plus(const(3),const(4)))).
Yes.
Or one could request multiple steps at once: 
?- step(plus(plus(const(1),const(2)),plus(const(3),const(4))),X), 
   step(X,Y), step(Y,Z).

X = plus(const(3), plus(const(3), const(4)))
Y = plus(const(3), const(7))
Z = const(10) 

Yes

Q: In the fourth line of rules, we have e1 e2 → e'1 e2. This looks like multiplication, but that was already done in the second line of rules.

A: Yes, it's not multiplication. All the rules in the fourth line concern application. In your Prolog code, you will use apply(E1,E2) etc.