Differences

This shows you the differences between two versions of the page.

--- teaching:is:ind-solutions [2020/06/24 16:35]
Franconi Enrico [12.6]
+++ teaching:is:ind-solutions [2020/06/24 17:11] (current)
Franconi Enrico [12.9]
@@ Line 110: / Line 110: @@
   yes(r105) ⇐
+<nowiki>(c)</nowiki>
+...similar to (d)...
+(d)
+  yes(R) ⇐ west(r107,R)  (*)
+     resolve with west(W1,E1) ⇐ imm_west(W1,E1).
+     substitution: {W1/r107,E1/R}
+  yes(R) ⇐ imm_west(r107,R)
+     resolve with imm_west(r107,r109)
+     substitution: {R/r109}
+  yes(r109) ⇐
+Another derivation by backtracking to (*) and selecting another clause to resolve against:
+  yes(R) ⇐ west(r107,R)  (*)
+     resolve with west(W1,E1) ⇐
+          imm_west(W1,M1) ∧
+          west(M1,E1).
+     substitution: {W1/r107,E1/R}
+  yes(R) ⇐ imm_west(r107,M1) ∧ west(M1,R).
+     select leftmost conjunct
+     resolve with imm_west(r107,r109)
+     substitution: {M/r109}
+  yes(R) ⇐ west(r109,R).
+    resolve with west(W2,E2) ⇐ imm_west(W2,E2).
+     substitution: {W2/r109,E2/R}
+  yes(R) ⇐ imm_west(r109,R)
+     resolve with imm_west(r109,r111)
+     substitution: {R/r111}
+  yes(r111) ⇐
 ===== 12.8 =====
+(a)
+  f(X,X,c,X,c)
+(b)
+  yes(c(l,X1),L) ⇐ append(c(l,X1),c(L,nil),c(l,c(i,c(s,c(t,nil)))))
+<nowiki>(c)</nowiki>
+  append(c(l,X1),c(L,nil),c(l,c(i,c(s,c(t,nil))))) ⇐
+     append(X1,c(L,nil), c(l,c(i,c(s,c(t,nil)))))
 ===== 12.9 =====
+(a)
+  {Z/f(X),Y/g(b)}
+(b)
+  {W/f(t),X/t,Q/t}
+<nowiki>(c)</nowiki>
+  {P/val(X,bb),Z/val(X,bb)}
 ===== 12.14 =====
+(a) Here is a top-down derivation:
+  yes(Y) ⇐ adj(b,Y,c(a,c(b,c(b,c(a,emp))))).
+    choose clause 3, with { A/b,B/Y,L/c(a,c(b,c(b,c(a,emp)))),F/F1,E/E1 }
+  yes(Y) ⇐ ap(F1,c(b,c(Y,E1)),c(a,c(b,c(b,c(a,emp)))))
+    choose clause 2, under
+    { F1/c(a,T2),L/c(b,c(Y,E1)),H/a,R/c(b,c(b,c(a,emp))),T/T2 }
+  yes(Y) ⇐ ap(T2,c(b,c(Y,E1)),c(b,c(b,c(a,emp))))   (*)
+    choose clause 1 under { T2/emp,Y/b,E1/c(b,c(a,emp)) }
+  yes(b) ⇐
+(b) Yes, there is one more answer .
+  at (*)
+    choose clause 2 under
+    { T2/c(b,T3),L/c(b,c(Y,E1)),H/b,R/c(b,c(a,emp)),T/T3 }
+  yes(Y) <- ap(T3,c(b,c(Y,E1)),c(b,c(a,emp)))
+    choose clause 1 under { T3/emp,L/c(b,c(a,emp)),Y/a,E1/emp
+  yes(a) <-

FranconiSpace

User Tools

Site Tools

Differences

Page Tools