Feature structure unification in minikanren

Question

How would one define a feature structure unification and subsumption in minikanren if we represent feature structures with lists?

The general behaviour would be something like this (I think):

(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))

---

The following code sort of works, but backwards unification gets stuck when ran with 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)))])))

Answer 1

You can implement this by modifying the code for unification in your minikanren implementation.

I would recommend not using lists to represent feature structures though, instead you could define a new record type than holds a list that always terminates in a fresh variable and one of these would represent a feature structure. Then you can still use lists and other objects as well as having these new objects available.

When the unification code sees two feature structures it would need to unify all the matching keys recursively and extend the 'rest' part of each one to contain the fields unique to the other feature structure (no destructive mutation).