scheme - minikanren中的特征结构统一
问题描述
如果我们用列表表示特征结构,我们将如何在 minikanren 中定义特征结构统一和包含?
一般行为将是这样的(我认为):
(run* (q) (unifyo '(a b) '(a b) q))) => (a b)
(run* (q) (unifyo '(x (a b)) '(x (c d)) q)) => (x (a b) (c d)) (x (c d) (a b))
(run* (q) (unifyo '(x (a b)) '(x (a d)) q)) => () ; fails because '(a b) is
; incompatible with '(a d)
(run* (q)
(fresh (y) (unifyo '(x (a b)) `(x ,y) q)) => (x (a b)))
(run* (q) (unifyo q '(x (a b)) '(x (a b) (c d)))) => (x (c d))
以下代码可以正常工作,但是在使用 run* 运行时,向后统一会卡住:
;; unifies f1 with l2
(define unify-f-with-list°
(lambda (f1 l2 out)
(conde
[(== '() l2) (== `(,f1) out)]
[(fresh (la ld a2 d2 a1 d1 res)
(=/= '() l2)
(== `(,la . ,ld) l2)
(== `(,a2 . ,d2) la)
(== `(,a1 . ,d1) f1)
(conde
[(== a2 a1)
(== `(,res . ,ld) out)
(unify° f1 la res)]
[(fresh ()
(=/= a2 a1) ;; if not
(== `(,la . ,res) out)
(unify-f-with-list° f1 ld res))]))])))
(define unify-list-with-list°
(lambda (l1 l2 out)
(conde
[(== '() l1) (== l2 out)]
[(== '() l2) (== l1 out)]
[(fresh (a1 d1 res)
(=/= '() l1)
(== `(,a1 . ,d1) l1)
(unify-f-with-list° a1 l2 res)
(unify-list-with-list° d1 res out))])))
(define unify°
(lambda (f1 f2 out)
(conde
[(== f1 f2) (== f1 out)]
[(fresh (a1 d1 a2 d2)
(=/= f1 f2)
(== `(,a1 . ,d1) f1)
(== `(,a2 . ,d2) f2)
(== a1 a2)
(fresh (res)
(unify-list-with-list° d1 d2 res)
(== `(,a1 . ,res) out)))])))
解决方案
您可以通过修改 minikanren 实现中的统一代码来实现这一点。
不过,我建议不要使用列表来表示特征结构,而是可以定义一个新的记录类型,而不是保存一个始终以新变量终止的列表,其中一个表示特征结构。然后,您仍然可以使用列表和其他对象以及使这些新对象可用。
当统一代码看到两个特征结构时,它需要递归地统一所有匹配的键并扩展每个的“其余”部分以包含另一个特征结构唯一的字段(无破坏性突变)。
推荐阅读
- javascript - Regex101.com 和 Chrome 输出不同
- python - Python文件描述符开闭操作,分块上传文件
- angular - 使用自动完成和“updateOn:'blur'”时防止早期验证
- javascript - 在函数内发生更改后无法访问更改的变量值
- javascript - 设置属性时设置所有同名属性的Javascript对象
- python - 如何通过按 Tkinter 中的按钮将 Var 显示到标签中
- android - 建立警告?
- mysql - Xampp MySQL 未启动 - “MYSQL 未在 XAMPP 3.2.1 版本上启动……”
- php - 如何获得特定值数组的总和
- elasticsearch - 弹性搜索是否将索引和文档都保存在缓存中?