Skip to content
Snippets Groups Projects
Commit 71d22929 authored by Michael Leuschel's avatar Michael Leuschel
Browse files

add more text about substitutions 


Signed-off-by: default avatarMichael Leuschel <leuschel@uni-duesseldorf.de>
parent 08c5cf0c
No related branches found
No related tags found
No related merge requests found
Show whitespace changes
Inline Side-by-side
logic_programming/7_Unification.ipynb
+ 17
− 13
View file @ 71d22929
%% Cell type:markdown id:9eb5530a tags:
This notebook is not finished yet and lacks some markdown explanations.
### Substitutions
Substitution: mapping from variables to terms
A *substitution* is a mapping from variables to terms.
We use the following notation for substitutions: {X1/t1, …, Xn/tn}
Notation: {X1/t1, …, Xn/tn}
Examples:
Examples of substitutions are:
{X/a} {X/b, Y/s(0)} {Y/Z} {}
In Prolog we represent this as lists of bindings:
Intuitively, ```{X/a}``` means we replace all occurences of X by a.
In Prolog we represent substitutions as lists of bindings.
E.g., we represent ```{X/a}``` by ```['X'/a]``` where ```/``` is a functor of arity 2.
The following Prolog predicate checks is something is a valid substitution:
%% Cell type:code id:78764141 tags:
``` prolog
is_subst([]).
is_subst([Var/Term|T]) :- variable(Var), term(Term), is_subst(T).
variable('$VAR'(_)).
variable('$VAR'(_)). % encode variables by this special functor
variable('X'). % a few artificial variables for easier reading
variable('Y').
variable('Z').
term(_). % no checks done at the moment; we allow any Prolog term, but suppose we have no real Prolog variables
```
%% Cell type:code id:b03ac6e7 tags:
``` prolog
?- is_subst(['X'/a]).
```
%% Output
%% Cell type:markdown id:ab0d39bc tags:
### Applying Substitutions
Applying a substitution to a term or wff
Instantaneous replacement by right-hand sides
Applying a substitution to a term or wff is done by
instantaneous and simultaneous replacement of all variables in the left-hand sides by the corresponding right-hand sides.
The following Prolog predicate applys a substitution to a term.
%% Cell type:code id:f6f156a3 tags:
``` prolog
% apply(Term,Subst,NewTerm)
apply(Var,Subst,Res) :- variable(Var), !,
(member(Var/New,Subst) -> Res=New ; Res=Var).
apply(Term,Subst,Res) :- Term =.. [Functor|Args],
l_apply(Args,Subst,NewArgs),
Res =.. [Functor|NewArgs].
l_apply([],_,[]).
l_apply([Arg1|T],Subst,[NewArg1|NewT]) :- apply(Arg1,Subst,NewArg1),
l_apply(T,Subst,NewT).
```
%% Cell type:code id:c675dc2a tags:
``` prolog
?- apply(p('X'),['X'/a],Res).
```
%% Output
%% Cell type:code id:9639129f tags:
``` prolog
?- apply(f('X',b,'Y',c,'X'),['X'/a],Res).
```
%% Output
%% Cell type:code id:a36930e8 tags:
``` prolog
?- apply(f('X','Y'),['X'/'Y','Y'/'X'],Res).
```
%% Output
%% Cell type:markdown id:c2f4b9a9 tags:
A substitution s is called a unifier of two terms (or wff’s) A and B iff As = Bs
A substitution s is called a *unifier* of two terms (or wff’s) A and B iff As = Bs
%% Cell type:code id:5a3f584e tags:
``` prolog
?- S=['X'/a],
apply(p('X'),S,Res1),
apply(p(a),S,Res2).
```
%% Output
%% Cell type:code id:5290b75d tags:
``` prolog
?- S=['X'/'Z', 'Y'/'Z'],
apply(p('X','Y'),S,Res1),
apply(p('Z','Z'),S,Res2).
```
%% Output
%% Cell type:markdown id:5fd84486 tags:
This is not a unifier:
%% Cell type:code id:347e1997 tags:
``` prolog
?- S=['X'/s('X')],
apply(p('X'),S,Res1),
apply(p(s('X')),S,Res2).
```
%% Output
%% Cell type:markdown id:96d07660 tags:
### Composing Substitutions
Composition s1s2 of two substitutions s1 and s2
is defined like composition of functions: A(s1s2) = (As1)s2
Let s1={X1/t1,...},s2={Y1/r1,...},
then s1s2 = {X1/t1s1,...}∪ {Yi/ri| Yi ∉ {X1,...} }
(and delete Xi/tis1 if Xi=tis1)
In Prolog this gives this (naive) implementation:
%% Cell type:code id:d56c09cb tags:
``` prolog
compose_subst(Sub1,Sub2,Res) :-
apply1(Sub1,Sub2,NewSub1), % apply Sub2 to RHS of Sub1
filter2(Sub2,Sub1,NewSub2), % filter unreachable parts of Sub2
append(NewSub1,NewSub2,Res).
apply1([],_,[]).
apply1([X1/T1|T],Sub2,Res) :- apply(T1,Sub2,NewT1),
(NewT1=X1 -> apply1(T,Sub2,Res) % X1/NewT1 is useless; remove it
; Res = [X1/NewT1|ResT], apply1(T,Sub2,ResT)).
filter2([],_,[]).
filter2([Y1/T1|T],Sub1,Res) :-
(member(Y1/_,Sub1) -> filter2(T,Sub1,Res) % Y1 is in domain of Sub1
; Res=[Y1/T1|ResT], filter2(T,Sub1,ResT)).
```
%% Cell type:code id:b1f992d9 tags:
``` prolog
?- compose_subst(['X'/a],['Y'/b],Res).
```
%% Output
%% Cell type:code id:df25466a tags:
``` prolog
?- compose_subst(['X'/'Y'],['Y'/b],Res).
```
%% Output
%% Cell type:code id:c6a79cdf tags:
``` prolog
?- compose_subst(['X'/'Y'],['Y'/'X'],Res).
```
%% Output
%% Cell type:code id:68a10c4f tags:
``` prolog
?- compose_subst(['X'/f('X')],['X'/a],Res).
```
%% Output
%% Cell type:markdown id:778e0b71 tags:
### Robinson's Unification Algorithm
A (naive) Prolog version of the unification algorithm.
It does not really compute the disagreement tuple; it traverses both terms and applies the current substitution as it goes along.
%% Cell type:code id:0f59567c tags:
``` prolog
unify(X,Y,SubSoFar,Res) :-
apply(X,SubSoFar,NX),
apply(Y,SubSoFar,NY),
unify2(NX,NY,SubSoFar,Res).
unify2(X,Y,SubSoFar,Res) :- X==Y,!,
Res=SubSoFar. % there are no disagreements at this position; keep the current substitution
unify2(X,Y,SubSoFar,Res) :- variable(X),!, % ak is a variable which does not occur in bk
not_occurs(X,Y),
compose_mgu(SubSoFar,[X/Y],Res).
unify2(X,Y,SubSoFar,Res) :- variable(Y),!, % bk is a variable which does not occur in ak
not_occurs(Y,X),
compose_mgu(SubSoFar,[Y/X],Res).
unify2(FX,FY,SubSoFar,Res) :-
FX =.. [Func|ArgsX],
FY =.. [Func|ArgsY], % check we have the same function symbol and proceed unifying arguments
l_unify(ArgsX,ArgsY,SubSoFar,Res).
compose_mgu(SubSoFar,New,Res) :-
compose_subst(SubSoFar,New,Res),
format('Adding binding ~w, new candidate MGU ~w~n',[New,Res]).
l_unify([],[],Sub,Sub).
l_unify([X1|TX],[Y1|TY],Sub,Res) :-
unify(X1,Y1,Sub,Sub2),
l_unify(TX,TY,Sub2,Res).
occurs(X,Y) :- X==Y,!.
occurs(X,FY) :- FY =.. [_|Args], member(Y,Args), occurs(X,Y).
not_occurs(X,Term) :- \+ occurs(X,Term).
```
%% Cell type:code id:ca8373d0 tags:
``` prolog
?- occurs('X',f('X')).
```
%% Output
%% Cell type:code id:e2e2a0fe tags:
``` prolog
?- unify(f('X'),f(a),[],Res).
```
%% Output
%% Cell type:code id:e04a20d1 tags:
``` prolog
?- unify(f(a),'X',[],Res).
```
%% Output
%% Cell type:code id:c2b9d14f tags:
``` prolog
?- unify(f('X'),'Y',[],Res).
```
%% Output
%% Cell type:code id:126098d1 tags:
``` prolog
?- f(X)=Y.
```
%% Output
%% Cell type:code id:679ece73 tags:
``` prolog
?- unify(f('Y',s('Y')),f('X',s(s(0))),[],Res).
```
%% Output
%% Cell type:code id:89c66d0d tags:
``` prolog
```
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment