15-819K: Logic ProgrammingLecture 16Substitution SemanticsFrank PfenningOctober 24, 2006In this lecture we introduce a semantics with an explicit substitution, inpreparation for presenting various program analyses later. The semanticswill have the property that its goals appear exactly as in the original pro-grams, with a separate subst itu tion as part of the judgment. We also re-viewed potential project areas during lecture, which is not represented inthese notes.16.1 Semantic LevelsWhen designing a program analysis we need to consider which level of se-mantic description is appropriate. This is relevant both for designing andproving the correctness of the analysis, which could be e ither simple ordifficult, depending on our starting point. By the “level of semantic de-scription” we mean here the spectrum fro m the logical semantics (in whichwe can only talk about truth), through one where subgoal order is exp licit,to one with a failure continuation. An additional dimension is if a substi-tution is e x plicit in the se mantics.Which kind of semantics is appropriate, for example, for defining modeanalysis? We would like to stay as high-level as possible, while still beingable to express the property in question. Because mode analysis dependson s ubgoal order, one would expect to make subgoal order explicit. More-over, since groundedness is a property of the substitution that is applied,we also should make a substitution explicit during computation. On theother hand, modes do not interact with backtracking, so we do not expectto need a failure continuation.We take here a slight sh ortcut, using a semantics with an explicit sub-stitution, but not a subgoal stack. Of course , it is possible to g ive such aLECTURE NOTES OCTOBER 24, 2006L16.2 Substitution Semanticssemantics as well. Omitting the subgoal stack has the advantage that wecan relatively easily talk about the successful return of a predicate.16.2 A Substitution SemanticsThe semantics we give takes a goal G under a substitution τ. It produces asubstitution θ with the invariant that Gτθσ for any grounding substitutionσ. We define it on the fully residuated form, where fo r every predicate pthere is exactly one clause, and this clause has the form ∀x. p(x) ← G.In the judgment τ ` G / θ we maintain th e invariant that dom(τ) ⊇FV(G) and that Gτθ true where we mean that there is a proof paramet-ric in t h e remaining free variables. Moreover, θ substitutes only for logicvariables X.An important point1is that τ should substitute exactly for the originallyquantified variables of G, and not for logic variables introduced during thecomputation. This is the role of θ which substitutes only for logic variables.The rule for atomic predicates is on e place whe re this is important.(∀x. p(x) ← G) ∈ Γ tτ/x ` G / θτ ` p(t) / θWe see that, ind eed, the substitution on the premise accounts for all vari-ables in G by the assumption of a close d normal form for programs.The rule for conjunction presumes a subgoal order via the threading ofθ1, without using a subgoal stack.τ ` G1/ θ1τ[θ1] ` G2/ θ2τ ` G1∧ G2/ θ1θ2Here we have used a variant of the composition operator in order to main-tain o ur invariant on the input substitution. τ[θ1] applies θ1to every ele-ment of τ , but does not extend it. That is,(t1/x1, . . . , tn/xn)[θ] = (t1[θ]/x1, . . . , tn[θ]/xn)Truth is straightforward, as are th e rules for disjunction and falsehood.τ ` > / (·)τ ` G1/ θτ ` G1∨ G2/ θτ ` G2/ θτ ` G1∨ G2/ θno rule forτ ` ⊥ /1I missed this point in lecture, which is why the system I gave did not work quite as wellto prove the correctness of mode analysis.LECTURE NOTES OCTOBER 24, 2006Substitution Semantics L16.3The existential q uantifier introduces a fresh logic variable X. This logicvariable can somehow “es cape” in that it may occur in the domain or co-domain θ. Intuitively, this makes s ense because a logic variable that is no tinstantiated during the solution of G will remain after success.X 6∈ FV(τ) τ, X/x ` G / θτ ` ∃x. G / θFinally, equality reduces to unification.tτ.= sτ | θτ ` t.= s / θ16.3 CorrectnessThe substitution semantics from t h e previous section is sound and com-plete in relation to the logical s emantics of truth. First, the soundness. Asremarked above, truth of a proposition with free variables is defined para-metrically. That is, there must be one deduction with free variables everyground instance of which is true und er the usual ground interpretation.Theorem 16.1 If τ ` G / θ for dom(τ) ⊇ FV(G) then Gτθ true.Proof: By induction on the deduction D of τ ` G / θ. For unification, werely on soundness of unification. 2Completeness follows the usual pattern of lifting to deduction with freevariables.Theorem 16.2 If Gτσ true where dom(τ ) ⊇ FV(G) and cod(σ) = ∅ thenτ ` G / θ and σ = θσ0for some θ and σ0.Proof: By induction on th e deduction of Gτ σ θ. For unification we invokethe property that unification returns a most general unifier. 216.4 An Asynchronous Substitution SemanticsInstead of giving substitution on goals for the residuated s emantics, we canalso give it directly o n programs and goals if a normal form for programsis not desired or needed. There will be two judgments: τ ` A / θ where Afunctions as a goal, and τ ; A  P / θ where A is for mula under focus.LECTURE NOTES OCTOBER 24, 2006L16.4 Substitution Semanticsτ ` A1/ θ1τ[θ1] ` A2/ θ2τ ` A1∧ A2/ θ1θ2τ ` > / (·)omitted hereτ ` A1⊃ A2/omitted hereτ ` ∀x. A /τ; A  P / θ A ∈ Γτ ` P / θτ; A1 P / θτ; A1∧ A2 P / θτ; A2 P / θτ; A1∧ A2 P / θno rule forτ; >  P /X /∈ FV(τ) (τ, X/x); A  P / θτ; ∀x. A  P / θP0τ.= P τ | θτ; P0 P / θτ; A1 P / θ1τ[θ1] ` A2/ θ2τ; A2⊃ A1 P / θ1θ2We have not treated here implication and universal quantification as agoal. Implication is straightforw ard (see Exercise 16.1). Universal quantifi-cation in goals (which we have mostly avoided so far) creates difficultiesfor unification and is left to a futu re lecture.The correctness theorem for this version of t h e semantics is left to Exer-cise 16.2.16.5 ExercisesExercise 16.1 Extend the substitution semantics to permit dynamic assumptionsΓ and goals of the form A1⊃ A2. Take care to account for the possibility that thatdynamic assumptions may contain free variables.Exercise 16.2 State and prove the