[问题描述]

编程实现表达式合一算法，对任意两个表达式E1、E2，找出其最一般合一s

[测试数据]

输入表达式：

E1 = P (x,  f (x),  g (z) )       E2 = P (y,  f ( g (b) ),  y )

输出结果：

s = { g(b)/x ,  g(b)/y ,  b/z }

[实现提示]

1.用广义表结构存储表达式

例：

表达式E1 = P (x,  f (x),  g (z) ) ，可表示如下：

( P   x   ( f  x )   ( g  z) )

表达式E2 = P (y,  f ( g (b) ),  y ) ，可表示如下：

( P   y   ( f  ( g  b ) )   y )

2.用广义表结构存储合一(代换)

例：s = { g(b)/x ,  g(b)/y ,  b/z } ，可表示如下：

s = ( ( (g  b)  x)  ((g  b)  y)  (b  z) )

3.变量表示

置特性值 或 设变量表 或 与var构成序偶

假设使用变量表：

varlist = ( x  y  z  ……)

[测试用例] (unify  '(p  a  b)  '(p  x  y) )

[测试结果]

((A X) (B Y))

结果正确

代码：(以下是注释版本方便理解)

;;开始假设变量表：

(setq varlist '(x y z))

;;变量判断函数 isvar

;; 如果原子 a 是变量则返回真，否则返回假。

(defun isvar(a)

(if(member a varlist) t nil)

)

;;包含判断函数contain

;;判断e里面是否包含x

(defun contain(e x) ;; 或 (defun occur(y x)

(cond ( (null e) nil) ;;e为空，返回nil

( (atom e) (if(equal e x) t nil) ) ;;e为原子且e与x相同，返回t

;;e为原子且e与x不相同，返回nil

(t ;; 否则，当e不是空表也不是原子时

(cond

((contain (car e) x ) t);;递归，e的表头car中包含x，返回t

((contain (cdr e) x ) t) ;;递归，e的表尾cdr中包含x，返回t

(t nil)))));;都不包含，返回nil

;;card为表中第二个元素

;;替换算法subs ( e s1 ) ，其中 s1 是单个“变量代换对”，

;;采用递归处理，分别对表头、表尾进行代换，然后合并、返回。

(defun subs(e s1) ;; e为表达式，s1为单个代换

(let (new_head new_tail) ;;定义变量new_head和 new_tail

(cond ( (null e) nil);;e为空表，代换后结果为nil

( (atom e)(if (equal e (second s1)) (first s1) e ));;e为原子并且与s1的分母second相同 ,代换后结果为s1的分子first

;;否则，当e为原子并且与s1的分母不相同 代换后结果e

(t

(setq new_head (subs(car e) s1) )

(setq new_tail(subs(cdr e) s1) )

(cons new_head new_tail))) ) )

;;t 用 s1 对 e 的表头做代换得到新表头 new_head

;;用 s1 对 e 的表尾做代换得到新表尾 new_tail

;;用 cons 函数将 new_head 加到 new_tail 的前面

;;代换函数 substitution

;;利用迭代，进行替换

(defun substitution(m nlist)

(cond ((null nlist) m);;如果nlist为空表，返回m

(t (setq m (subs m (car nlist)));;如果不为空表，m值为nlist的表头替换到m的结果

(substitution m (cdr nlist)))));;迭代，将nlist的表尾替换到m

;;先写算法子函数cp1,将 s2 作用到 s1 的“分子”上

(defun cp1(s1 s2)

(let (ti vi new_ti);;定义三个变量ti vi new_ti

(cond ((null s1) '( ) );;如果s1为空，返回空表

(t (setq ti (caar s1)) ;; 如果s1不为空，取 s1 中表头代换的“分子”给ti,即表头的头

(setq vi (cdar s1)) ;; 取 s1 中表头代换的“分母”给vi，即表头的尾

(setq new_ti (substitution ti s2)) ;; 将 s2 作用到 ti 上得到的结果给new_ti

(cons (cons new_ti vi)( cp1 (cdr s1) s2) ))))) ;; 将新的表头代换加入新的表尾代换(表尾递归结果)合并

;;((合并new_ti与ti) , (递归调用cp1,对s1的尾部进行替换)),并返回结果

;;caar表头的头

;;cdar表头的尾

;;合成函数 compose ，先调用算法子函数cp1，然后让返回结果与s2取并集

(defun compose(s1 s2)

(let (new_s1) ;;定义new_s1

(setq new_s1 (cp1 s1 s2)) ;; 将 s2 作用到 s1 的“分子”上

(append new_s1 s2))) ;;将new_s1与s2合并，并返回结果

;;合一函数 unify

(defun unify(e1 e2)

(let

(bf f1 f2 t1 t2 s1 s2 g1 g2);;定义变量

(cond ((or (atom e1) (atom e2))

(when (not (atom e1)) (setq bf e1) (setq e1 e2) (setq e2 bf))

(cond

((equal e1 e2) '())

((and (isvar e1) (contain e2 e1)) 'fail)

((isvar e1) (list (list e2 e1)))

((isvar e2) (list (list e1 e2)))

(t 'fail)) )

(t

(setq f1 (car e1)) (setq t1 (cdr e1))

(setq f2 (first e2)) (setq t2 (rest e2))

(setq s1 (unify f1 f2))

(cond ((equal s1 'fail) 'fail)

(t

(setq g1 (substitution t1 s1))

(setq g2 (substitution t2 s1))

(setq s2 (unify g1 g2))

(if (equal s2 'fail) 'fail (compose s1 s2)))))) ) )

以下是实际代码：(用lispwork运行时不要写注释，可直接运行)

(setq varlist '(x y z))

(defun isvar(a)

(if(member a varlist) t nil)

)

(defun contain(e m)

(cond ( (null e) nil)

( (atom e) (if(equal e m) t nil) )

(t

(cond

((contain (car e) m ) t)

((contain (cdr e) m ) t)

(t nil)

)

)

)

)

(defun sb(e s1)

(let (head tail)

(cond ((null e) nil)

((atom e)(if (equal e (second s1)) (first s1) e ))

(t

(setq head (sb (car e) s1) )

(setq tail (sb (cdr e) s1) )

(cons head tail)

)

)

)

)

(defun substitution(e m)

(cond ((null m) e)

(t

(setq e (sb e (car m)))

(substitution e (cdr m))

)

)

)

(defun cp1(s1 s2)

(let (ti vi new_ti)

(cond ((null s1) '() )

(t

(setq ti (caar s1))

(setq vi (cdar s1))

(setq new_ti (substitution ti s2 ))

(cons (cons new_ti vi) (cp1 (cdr s1) s2)

)

)

)

)

)

(defun compose(s1 s2)

(let (new_s1)

(setq new_s1 (cp1 s1 s2))

(append new_s1 s2)

)

)

(defun unify(e1 e2)

(let (bf f1 f2 t1 t2 s1 s2 g1 g2)

(cond ( (or (atom e1) (atom e2))

(when (not (atom e1)) (setq bf e1) (setq e1 e2) (setq e2 bf))

(cond

((equal e1 e2) '())

((and (isvar e1) (contain e2 e1)) 'fail)

((isvar e1) (list (list e2 e1)))

((isvar e2) (list (list e1 e2)))

(t 'fail)

)

)

(t

(setq f1 (car e1)) (setq t1 (cdr e1))

(setq f2 (first e2)) (setq t2 (rest e2))

(setq s1 (unify f1 f2))

(cond ((equal s1 'fail) 'fail)

(t

(setq g1 (substitution t1 s1))

(setq g2 (substitution t2 s1))

(setq s2 (unify g1 g2))

(if (equal s2 'fail) 'fail (compose s1 s2))

)

)

)

)

)

)