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

Could you clarify what the three inputs mean, more precisely? In particular it's not clear what the form of the third argument is supposed to be. And also, what are "variables" and what are "atoms"? Why is `(a b)` compatible with `(c d)` in the 2nd example, but `(a b)` is incompatible with `(a d)` in the 3rd example? — Alex Knauth, Nov 25 '18 at 15:22
Could you explain each sample call's context and meaning? Include some links to define all the terms you're using? At least some link to some relevant page or something? — Will Ness, Nov 25 '18 at 16:26
I am talking about feature structures like [these](https://en.wikipedia.org/wiki/Feature_structure), and would like to have a prolog like functionality like [here](http://cs.union.edu/~striegnk/courses/nlp-with-prolog/html/node84.html#l11.sec.fs.prolog) — Matías Guzmán Naranjo, Nov 25 '18 at 17:53
The three inputs would be: (feature-structure-1 feature-structure-2 result-of-unification). A feature structure is an attribute-value pair. (a b) cannot unify with (a c), because for the same attribute, they have different values. (x (a b)) can unify with (x (c d)) because 'c and 'a are different. The prolog page explains this well. If we have [agr [number sg]] and unify it with [agr [person 3]] we should get [agr [number sg | person 3]]. — Matías Guzmán Naranjo, Nov 25 '18 at 18:00
for a possible Prolog implementation, see [`attr/2`](https://stackoverflow.com/a/20408402/849891). With it, the last example in 13.5.1 is achieved with `attr(X, [cat-s, head-Head]), attr(Head, [agr-Agr, subj-Subj]), attr(Subj, [agr-Agr]), attr(Agr, [num-sg,pers-3]).`. or `maplist(attr, [X, Head, Subj, Agr], [[cat-s, head-Head], [agr-Agr, subj-Subj], [agr-Agr], [num-sg,pers-3]]).`. — Will Ness, Dec 01 '18 at 14:52
yes, there are several prolog implementations. But I'd really need this in minikanren. — Matías Guzmán Naranjo, Dec 01 '18 at 15:19
@MatíasGuzmánNaranjo Can you fix the fourth query that has a `y` variable that is not defined, please? — amirouche, Dec 10 '18 at 21:28

score 1 · Answer 1 · answered Dec 09 '18 at 00:41

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

answered Dec 09 '18 at 00:41

river

1,028
6
16

I've managed to write an almost working solution, but it gets stuck when querying backwards since it cannot figure out there is a finite number of solutions. Any ideas how to fix it? (I've added the code to my question). – Matías Guzmán Naranjo Dec 09 '18 at 19:26
2

@MatíasGuzmánNaranjo You are trying to implement this in minikanren. I don't recommend that. (It is not going to work well because mk doesn't have the non-logical control constructs prolog has like cut) Instead implement it in scheme as an additional feature to the minikanren system. – river Dec 09 '18 at 20:44
Why do you think 'cut' is necessary for this to work? And the whole point of this is to have a unification relation which can run in either direction. – Matías Guzmán Naranjo Dec 09 '18 at 21:00
2

I don't think you should use cut. The prolog code that you linked in the question uses cut. This feature structure stuff can't be expressed in purely logical mk code. That's why you need to drop down to the scheme implementation of unification to write this. If implemented correctly it will be bidirectional just like unification is. – river Dec 09 '18 at 22:42
1

the fact that the mk program doesn't terminate is AFAIK a clue that it requires cut. I agree with @rain1 and I think that the implementation must be done in scheme. – amirouche Dec 10 '18 at 21:20
Why can it not be expressed in mk code? Any concrete ideas on how to rewrite the unification in scheme? My guess about why it does not find the final answers is because it traverses only one of the lists, and unifies the features in that list with the second list, so unify° doesn't know it can also do the process the other way around. – Matías Guzmán Naranjo Dec 11 '18 at 20:10
@rain1 I thought `condu` emulates cut in minikanren. @matias But if you use it, it means it won't be bidirectional all by itself like pure predicates are... You could still write an interface predicate that would inspect the arguments, decide in which direction it has to work, and call the appropriate specific predicate. (in theory, in Prolog; don't know if minikanren has `var/1`, `ground/1` etc.). – Will Ness Dec 12 '18 at 07:19
avoid non-logical constructs like condu/condi/var/ground – river Dec 15 '18 at 23:51
"condi" perhaps you meant "conda". – Will Ness Dec 16 '18 at 10:55

Feature structure unification in minikanren

1 Answers1