15-819K: Logic ProgrammingLecture 4Operational SemanticsFrank PfenningSeptember 7, 2006In this lecture we begin in the ques t to formally capture the operationalsemantics in order to prove properties of logic programs that depend on theway proof search proceeds. This will also allow us to relate the logical andoperational meaning of programs to understand deeper properties of logicprograms. It will also form the basis to prove the correctness of variousform of program analysis, such as type checking or termination checking,to be introduced later in the class.4.1 Explicating ChoicesTo span t h e dist ance bet ween the logical and the operational semantics wehave to explicate a series of choices that are fixed when proof search pro-ceeds. We will proceed in this o rder:1. Left-to-right subgoal selection. In te r ms of inference rules, this meansthat we first search for a proof of the first premiss, then the second,etc.2. First-to-last clause selection and backtracking. In terms of inferencerules this means w h en more than one rule is applicable, we begin bytrying the one listed first, then the one listed second, etc.3. Unification. In terms of inference rules this means when we decidehow to instantiate the schematic variables in a rule and the unknownsin a goal, we use a particular algorithm to find the most gen eral uni-fier between the conclusion of the rule and the goal.LECTURE NOTES SEPTEMBER 7, 2006L4.2 Operational Semantics4. Cut. This has no reflection at the level of inference rules. We have tospecify how we commit to particular choices made so far when w eencounter a cut or another control constructs such as a conditional.5. Other built-in predicates. Prolog has other built-in predicates forarithmetic, input and o utput, changing the p rogram at run-time, for-eign function calls, and more which we will no t treat formally.It is useful not to jump directly to the most accurate and low-level se-mantics, because w e often would like to reason about properties of pro-grams that are independent of such detail. One set of examples we havealready seen: we can reaso n about the logical s emantics to e stablish prop-erties such as that t h e sum of t wo even numbers is even. In that case w e areonly interested in successful computations, and how we searched for themis not impor tant. Another example is represented by cut: if a program doesnot contain any cuts, the complexity of the semantics that captures it is un-warranted.4.2 Definitional IntpretersThe general methodology we follow goes back to Reynolds [3], adaptedhere to logic programming. We can write an interpreter for a languagein the language itself (or a very similar language), a so-called definitionalinterpreter, meta-interpreter, or meta-circular interpreter. This may fail t o com-pletely determine the behavior of the language we are s tudying (the objectlanguage), because it may dep end on the behavior of the language in whichwe write the definition (the meta-language), and the two are t h e same! Wethen transform the definitional interpreter, removing some of the advancedfeatures of the language we are defin ing , so that now the more advancedconstructs are explained in t erms of simpler ones, removing circular as-pects. We can interate the process until we arrive at the desired level ofspecification.For Prolog (although not pure first-o rder logic programming), the sim-plest meta-interpreter, hardly d eserving the name, issolve(A) :- A.To interpret the argument to solve as a goal, we simply execute it using themeta-call facility of Prolog.This does not provide a lot of insight, but it brings up the first issue:how do we represent logic programs and goals in order to execute themLECTURE NOTES SEPTEMBER 7, 2006Operational Semantics L4.3in our definitional interpre ter? In Prolog, the answer is e asy: we think ofthe comma which separates the subgoal of a clause as a binary functionsymbol den oting conjunction, and we think of the constant true which al-ways succeeds as just a constant. One can think of this as replicating thelanguage o f predicates in the language of function symbols, or not distin-guishing between th e two. The code above, if it were formally justifiedusing higher-order logic, would take the latter approach: logical connec-tives are data and can be treated as such. In the next interpreter w e takethe first approach: we overload comma to sep arate subgoals in the meta-language, but we also use it as a function symbol to describe conjunctionin the object language. Unlike in the code above, we w ill not mix the two.The logical constant true is similarly overloaded as a predicate constant ofthe same name.solve(true).solve((A , B)) :- solve(A), solve(B).solve(P) :- clause(P, B), solve(B).In the second clause, the head sol ve((A , B)) employs infix notation,and could be written equivalently as solve(’,’(A, B)).1The additionalpair of parentheses is necessary since solve(A , B) would be incorrectlyseen as a predicate solve with two arguments.The predicate clause/2 is a built-in predicate of Prolog.2The subg oalclause(P, B) will unify P w ith the head of each program clause and Bwith the corresponding body. In ot h er words, if cl ause(P, B) succeeds ,then P :- B. is an instance of a clause in the current program. Prolog willtry to unify P and B with the clauses of the current program first-to-last,so that the above meta-interpreter will work correctly with respect to theintuitive semantics explained earlier.There is a small amount o f standardization in that a clause P . in theprogram with an empty body is treated as if it were P :- true.This first interpreter does not really explicate anything: the order inwhich subgoals are solved in the object language is the same as the orderin the meta-language, according to the second clause. The order in whichclauses are tried is the order in wh ich clause/2 delivers them. And unifi-cation betw een the goal and the clause head is also inherited by the object1In Prolog, we can quote an infix operator to use it as an ordinary function or predicatesymbol.2In Prolog, it is customary to write p/n when refering to a p red icate p of arity n, sincemany predicates have different meanings at different arities.LECTURE NOTES SEPTEMBER 7, 2006L4.4 Operational Semanticslanguage from the meta-language through the unification carried out byclause(P, B) betwee n its first argument and th e clause heads in the pro-gram.4.3 Subgoal OrderAccording to ou r ou tline, the first task is