Homework # 12
due Tuesday, May 4, 4:00 PM

Reprise: Unification, Resolution and Solve

In this section, we are working with a predicate for ``flattening'' a tree where internal nodes have the form branch($V$,$W$) and leaves have the form leaf($X$). The flattened form is a list of all the items that show up in leaves. The predicate uses a helper predicate flattenH that takes an extra accumulator list (for efficiency).

  1. Give the results of the following calls to unify:
    1. unify(flattenH(leaf(X1),L1,[X1|L1]),flattenH(T,[],[1,2,3]))
    2. unify(flattenH(branch(V2,W2),L2,N2),flattenH(T,[],[1,2,3]))
    3. unify(flattenH(leaf(X3),L3,[X3|L3]),flattenH(W2,[],M2))
  2. Using the previous calls, give the results of the following calls to resolution:
    1. resolution([flattenH(leaf(X1),L1,[X1|L1])], [flattenH(T,[],[1,2,3])])
    2. resolution([flattenH(branch(V2,W2),L2,N2),
                  flattenH(W2,L2,M2),
                  flattenH(V2,M2,N2)],
                 [flattenH(T,[],[1,2,3])])
    3. resolution([flattenH(leaf(X3),L3,[X3|L3])],
                 [flattenH(W2,[],M2), flattenH(V2,M2,[1,2,3])])
  3. Using the previous steps to give the whole proof tree trace up to the first success for the following call. Please trace every call to solve, resolution and unify, even ones that fail.
    solve([flattenH(T,[],[1,2,3])])
    Assume the program consists of only the following rules: 
    
flattenH(leaf(X),L,[X|L]).
flattenH(branch(V,W),L,N) :- flattenH(W,L,M), flattenH(V,M,N).
  4. After this first success, the proof tree goes on forever without any more success. (Try it in Prolog!) Why?
This question is not graded as part of this Homework. Instead, your Homework # 10's grade will be increased by up to 50% of the points lost on the written part. For example, if you got 11 points out of 25 on the written part, you can gain up to 7 additional points by doing this part.

Natural Semantics

Do Exercise 23.1 (page 520) and Exercise 23.2 parts (b) and (c). For 23.2(b), use if, lt, and minus as the AST nodes, and use true and false as new potential values.

Put the complete Language Four interpreter in four.pl, as well as giving the additional natural semantic rules on paper. The source for the Language Three interpreter is available in

/afs/cs.uwm.edu/users/classes/cs431/src/homework12/three.pl

Small-Step Semantics

A small-step semantics work by returning the program with one step of evaluation done. Function calls and let's work by substituting the value for the variable into the body. The output is always an AST. To evaluate fully, one applies the small-step rules until no other rule is possible, which happens when there is a type error, or we end up with a value such as const(42). There are two kinds of values for Language Three: constants and functions.

The small-step semantics for Language Three is as follows, where $e$ means any expression, and $v$ means the expression must be a value, and $n$ means the expression must be an integer constant. \begin{mathpar} \inferrule{e_1 \to e'_1}{\texttt{$e_1$+$e_2$} \to \texttt{$e'_1$... ...$v_1$+$e'_2$}} \par\inferrule{ }{\texttt{$n_1$+$n_2$}\to{n_1+n_2}} \end{mathpar} \begin{mathpar} \inferrule{e_1 \to e'_1}{\texttt{$e_1$*$e_2$} \to \texttt{$e'_1$... ..._2} \par\inferrule{ }{\texttt{(fn $x$\ => $e$)}\,v \to e[x \to v]} \end{mathpar} Implement these rules in Prolog. The predicate step(E1,E2) should be true if E1 goes to E2 in one step, or as written mathematically: \( e_1 \to e_2 \). Write a second predicate eval(E,V) that is true if E goes to V in zero or more steps and V cannot be evaluated further. Hint: you will need to write a predicate isValue(E) that is true for values, and a predicate subst(E1,X,E2,E3) which unifies E3 with the result of substituting X with E2 everywhere it occurs in E1 (except inside of functions or ``let''s with formal parameter equal to X). Test your code, in particular using the examples from pages 510 and 512, and the following erroneous terms:


let(f,const(3),apply(var(f),const(4)))

let(x,const(3),plus(var(x),var(y)))

Submitting Your Work

You submit your program work by putting it in the homework12 directory in your AFS class volume. You may do all your work in this directory, or you may wish to do your work in a different directory and copy things when correct into this directory. In any case, you will lose permission to write things in this directory after the deadline, which is 4:00pm on Tuesday, May 4th. In other words, you must be done before lecture starts.

The homework12 directory should include the following:

About this document


John Tang Boyland
2004-04-30