```unify←{⎕IO ⎕ML←0 1              ⍝ Unification of expressions.

uni←{                       ⍝ unify exprs.
dis←⌽⍺⍺ disagree⌽⍺ ⍵    ⍝ vector of disagreement pairs.
0=⍴dis:⍺                ⍝ none: finished.
var val←pair↑ochk/¨dis  ⍝ select first pair.
new←var subs val        ⍝ derive subs function.
(new ⍺)∇ new ⍵          ⍝ retry after substitution.
}

disagree←{                  ⍝ disagreement pairs.
vars←isvar¨⍵            ⍝ terms are vars?
vars≡1 1:(~≡/⍵)/⊂⍵∩⍺⍺   ⍝ both: dis-pair if distinct.
1∊vars:,⊂(vars⍳1)⌽⍵     ⍝ one var: var-value pair.
0∊≡¨⍵:⍬ chk≡/⍵          ⍝ matching atomic terms: ignore.
≡/⍴¨⍵:↑,/,∇¨↓⍉↑⍵        ⍝ conformable: compare sub-terms.
err 5                   ⍝ otherwise: length error.
}

pair←⍺∘∇{                   ⍝ first disagreement pair.
dups←{⍵∊⊂⊃⍵}⊃¨⍵         ⍝ duplicate variables.
1=+/dups:⊃⍵             ⍝ first pair not duplicated: done.
⍺⍺ dups/⍵               ⍝ unify duplicate values.
}

subs←{                      ⍝ substitute [⍵⍵/⍺⍺] ⍵.
isvar ⍵:(⍵≡⍺⍺)⊃⍵ ⍵⍵     ⍝ variable: subs if match.
↑∇¨/(⍳×|≡⍵),⊂⍵          ⍝ substitute atom-wise.
}

occurs←{                    ⍝ var ⍺⍺ occurs in value ⍵.
isvar ⍵:⍺⍺≡⍵            ⍝ variable: check match.
1∊↑∇¨/(⍳×|≡⍵),⊂⍵        ⍝ check value atom-wise.
}

ochk←{⍺ ⍵ chk~⍺ occurs ⍵}   ⍝ occurs check.
chk←{⍵:⍺ ⋄ err 11}          ⍝ error unless ⍵.
err←'Can''t unify'∘⎕SIGNAL  ⍝ error function.
isvar←∊∘⍺∘⊂                 ⍝ check for var.

↑⍺ uni/⍵                    ⍝ unified expression.
}
code_colours

test script

Back to: notes

Back to: Workspaces
```