home *** CD-ROM | disk | FTP | other *** search
/ rtsi.com / 2014.01.www.rtsi.com.tar / www.rtsi.com / OS9 / OSK / EFFO / forum16.lzh / SOFTWARE / PROLOG / EXAMPLES / unify.pro < prev   
Text File  |  1991-03-24  |  5KB  |  111 lines
  1. /* 
  2.   Testimplementierung eines Unifikationsalgorithmus in Prolog.
  3.   (UNIFY.PRO)
  4.  
  5.   Autor: M. Moser
  6.   Datum: 16.7.90
  7.   Version: 1.0
  8.  
  9.   Historie:
  10.     Version 1.0 am 16.7.90: Urversion
  11. */
  12.  
  13. /* Ein Term ist definiert als eine Konstante oder ein Term aus      */
  14. /* einem Funktor und einer Liste von Termen als Argumente.  (Vgl.   */
  15. /* Terme in Prolog.)  Zwei Terme s und t heissen unifizierbar, wenn */
  16. /* es Substitutionen fuer die Variablen von s und t gibt, so dass s */
  17. /* und t gleich werden.  Eine Substitution fuer eine Variable x ist */
  18. /* ein Paar x/u, wobei u der Term ist, durch den x ersetzt wird.    */
  19. /* Der Term u darf aber selbst die Variable x nicht enthalten, da   */
  20. /* sich sonst eine unendliche Einsetzung ergaebe.  (Diese Situation */
  21. /* wird auch als loop bezeichnet.)  Stehen sich an entsprechenden   */
  22. /* Positionen von s und t zwei verschiedene Funktoren oder Konstan- */
  23. /* ten gegenueber, dann scheitert die Unifikation an einem sog.     */
  24. /* clash, denn derartige Terme lassen sich durch Variablenerset-    */
  25. /* zugen nicht gleich machen.                                       */
  26. /* Eine Menge M von Substitutionen wird auf einen Term t angewen-   */
  27. /* det, indem gleichzeitig alle Variablen von t durch die entspre-  */
  28. /* chenden Terme aus M ersetzt werden.  Die Anwendung von M auf t   */
  29. /* wird im weiteren als t M geschrieben.  M ist ein Unifikator      */
  30. /* zweier Terme s und t, wenn s M = t M ist, also die Substitutio-  */
  31. /* nen in M die Terme s und t gleich machen.  Ein allgemeinster     */
  32. /* Unifikator zweier Terme s und t ist schliesslich ein Unifika-    */
  33. /* tor M, so dass fuer jeden anderen Unifikator N von s und t gilt: */
  34. /* Es gibt einen Unifikator M', so dass t M M' = t N.  (Intuitiv    */
  35. /* gesprochen ist ein Unifikator genau dann ein allgemeinster Uni-  */
  36. /* fikator, wenn er moeglichst wenige Variablen durch moeglichst    */
  37. /* allgemeine Terme ersetzt.  Ein Term ist um so weniger allgemein, */
  38. /* je mehr Funktoren er enthaelt.)  Ein allgemeinster Unifikator    */
  39. /* ist bis auf Variablenumbenennungen eindeutig.                    */
  40.  
  41. /* Beispiele: (Der Versuch, zwei Terme s und t zu unifizieren,      */
  42. /*             wird unify(s, t) geschrieben.)                       */
  43. /*     unify(c, d)    -> clash   (zwei verschiedene Konstanten sind */
  44. /*                               nicht unifizierbar)                */
  45. /*     unify(x, c)    -> { x/c } (mit einer Variable ist jeder Term */
  46. /*                               unifizeribar,                      */
  47. /*     unify(x, f(x)) -> loop    sofern er die Variable nicht ent-  */
  48. /*                               haelt!)                            */
  49. /*     unify(f(x, c), g(h(y), y))                                   */
  50. /*                    -> { x/h(y), y/c }                            */
  51. /*     unify(x, y)    -> { x/y } oder { y/x }                       */
  52.  
  53. /* Der folgende Algorithmus gestattet es, zusaetzlich zu den beiden */
  54. /* Termen s und t noch eine Menge R bereits vorhandener Substitu-   */
  55. /* tionen anzugeben.  Als Ergebnis der Unifikation wird bei unifi-  */
  56. /* zierbaren Termen eine Liste Q von Substitutionen geliefert, an-  */
  57. /* derenfalls scheitert das Praedikat unify.                        */
  58.  
  59. unify(S, T, R, Q) :-
  60.     deref(S, R, U), deref(T, R, V), 
  61.     unifyterms(U, V, R, Q).
  62.  
  63. deref(S, [], S) :-
  64.     var(S).
  65. deref(S, _, S) :-
  66.     nonvar(S).
  67. deref(S, [bind(V, T) | R], T) :-
  68.     var(S), S == V.
  69. deref(S, [bind(U, _) | R], T) :-
  70.     var(S), S \== U, 
  71.     deref(S, R, T).
  72.  
  73. unifyterms(V, W, R, R) :-
  74.     var(V), var(W), V == W.
  75. unifyterms(V, W, R, [bind(V, W) | R]) :- 
  76.     var(V), var(W), V \== W.
  77. unifyterms(V, T, R, [bind(V, T) | R]) :- 
  78.     var(V), nonvar(T), 
  79.     not occurs(V, T, R).
  80. unifyterms(T, V, R, [bind(V, T) | R]) :-
  81.     nonvar(T), var(V), 
  82.     not occurs(V, T, R).
  83. unifyterms(S, T, R, Q) :-
  84.     nonvar(S), nonvar(T), 
  85.     functor(S, F, N), functor(T, F, N),
  86.     unifyargs(N, S, T, R, Q).
  87.  
  88. unifyargs(0, S, S, R, R).
  89. unifyargs(N, S, T, R, Q) :-
  90.     N > 0, M is N - 1, unifyargs(M, S, T, R, P),
  91.     arg(N, S, A), arg(N, T, B), unify(A, B, P, Q).
  92.  
  93. occurs(V, W, R) :-
  94.     var(V), var(W), V == W.
  95. occurs(V, W, R) :-
  96.     var(V), var(W), V \== W,
  97.     bound(W, R, T), occurs(V, T, R).
  98. occurs(V, T, R) :-
  99.     var(V), nonvar(T), 
  100.     functor(T, F, N), occursinargs(N, V, T, R).
  101.  
  102. bound(V, R, T) :-
  103.     deref(V, R, T), V \== T.
  104.  
  105. occursinargs(N, V, T, R) :-
  106.     N > 0, M is N - 1, occursinargs(M, V, T, R)
  107.     ;
  108.     arg(N, T, A), occurs(V, A, R).
  109.     
  110.  
  111.