1

A Functional Implementation of
Function-as-Constructor Higher-Order Uniﬁcation

Makoto Hamana
Department of Computer Science,
Gunma University, Japan
September 3, UNIF 2017, Oxford

2This Work
B [Libal and Miller FSCD’16]: A new decidable class of higher-order
uniﬁcation problems, Functions-as-Constructors uniﬁcation (FCU)
B Report here that FCU uniﬁcation can be implemented functionally
B SOL: Haskell-based tool for analysing conﬂuence and terminationof second-order computatoin rules– HO version of Knuth and Bendix’s critical pair checking
using FCU uniﬁcation

3Example: Computation Rules on Sum types

caseinl: a1 + a2 , (a1 → c), (a2 → c) → c: a1 → a1 + a2
inr : a2 → a1 + a2

(caseL) case(inl(X), F, G)(caseR) case(inr(Y ), F, G)(sumEta) case(Z, λx.H[inl(x)], λy.H[inr(y)])⇒ F (X)⇒ G(Y )⇒ H[Z]

λx.H[inl(x)], λx.H[inr(y)] are not higher-order patterns

4Higher-Order Patterns [Miller’91]
B A higher-order patternis a term where every application is of the form M [x1 , . . . , xn ]i.e.
a free variable M applied to distinct bound variables x1 , . . . , xn .
B Not HO patterns– M [N ]– M [cons(x, y)]– λx.H[inl(x)]– λy.H[inr(y)]5FC patterns [Yokoyama et al. ’04][Libal, Miller ’17]
B An FC pattern is a term p,
where every occurrence of M [t1 , . . . , tn ] in p:(i) every ti is a term without binders or free variables,
can contain fun. syms with arity n > 0 and bound variables(ii) every ti contains at least one bound variable,(iii) ti E
6 tj for every 1 ≤ i, j ≤ n.
B FC patterns:
λx.y.M [cons(x, y)]λx.H[inl(x)]B Not FC patterns:
M [N ]
λx.M [x, x]

M [nil]λy.H[inr(y)]λx.M [x, c(x)]6FC Pattern Matching and NoticeThm. [Yokoyama et al. Inf. Process. Lett.’04]?

Any second-order FC pattern matching problem p = t between an
FU pattern p and a λ-term t is decidable andhas a single most general matcher if matchable.
But the uniﬁcation between FC patterns?

x.y.M [c(x), c(y)] = x.y.c(N [y, x])
has at least two incomparable uniﬁers:{M 7→ x.y.y, N 7→ x.y.x} and {M 7→ x.y.x, N 7→ x.y.y}.

7

FCU Uniﬁcation
B Libal and Miller’ Functions-as-Constructors Uniﬁcation(FCU) [FSCD’16]?

B A FCU uniﬁcation problem is s = t
where s and t are FC patterns and satisﬁes:?

– Global restriction: in s = t, for every two diﬀerent
occurrences of applications M [s1 , . . . , sn ] and N [t1 , . . . , tm ],si C
6 tj holds
B Thm. An FCU uniﬁcation problem is decidable and ensures theexistence of a most general uniﬁer if solvable.
B Yokoyama et al.’s example actually violates the global restriction?

x.y.M [c(x), c(y)] = x.y.c(N [y, x])8Implementation
B Written in Haskell (about 500 lines)
B as a part of SOL system
B Algorithm in [Libal,Miler’16] is not immediately ready
B Base Nipkow’s ML implementation of pattern uniﬁcation– a basic library and infrastructure for higher-order uniﬁcation– e.g. on-the-ﬂy α-conversion and η-expansion.

9FCU Algorithm
a slight modiﬁcation of Libal and Miller’s, adapted to Nipkow’s
formalism?

(idem)

Q∀

t=t →

Q∀

[]

(abs)

Q∀

x, Q∀

s=t

(fun)

Q∀

(ﬂex-rigid)Q∀

λx.s = λx.t →→−?
−f →s =f t →→− ?
−F t =f →s →(ﬂex-ﬂex=) Q∀→− ?
−F t =F →s →(ﬂex-ﬂex6=)−
where →
z 0 = (zi | 1 ≤ i ≤ n, ti = si )→− ?
?
−F t =G→s →Q∀ s = tQ∀

?

Q∀

?

?

?

s1 = t1 , . . . , sn = tn

Q∀

[]

Q∀

[]

→− −
−
−
{F 7→ λ→z .discharge (zip t →z ) (f →s )}−{X 7→ λz1 , . . . , zn .H →z 0}→{Y 7→ λz1 , . . . , zm .H −z−ϕ(i) },where ϕ(j) = i if ti = sj for i = 1, . . . , n, j = 1, . . . , m.

10Actual Transformation Relation?

hQ∀ , (s = t) : E, θi- hQ0 , E 0 ++ (Eθ 0 ) ↓β , θ 0 ◦ θ i∀if hQ∀ , s = ti → hQ0∀ , E 0 , θ 0 i?

B (−) ↓β computes the β-normal form
B apply the “pruning’’ operation if applicable11Discharging
B→−s
Operation t|→−z

Yokoyama et al. [I. P. L. ’04] called“discharging”, gave a complicated algorithm−−
B Replace terms →s in t with variables →z.
B Similar to substitution of terms for variables,B→−sHence, implement t|→−z

as discharge θ tdischarge :: [(Term, Id)] -> Term -> Termdischarge th t’ = case lookup t’ th of
Just z -> O z
Nothing -> case t of
(x :.: t1) -> x :.: discharge th t1(t1 :@ t2) -> (discharge th t1) :@ (discharge th t2)t’-> t’12

Uniﬁcatoin Functionunif bvs (th,(s,t))?

processes a uniﬁcatoin problem hQ∀ , (s = t), θi.
unif :: [(Char,Id)] -> ([(Id, Term)], (Term, Term)) -> [(Id, Term)]
unif bvs (th,(s,t)) = case (devar th s,devar th t) of(x:.:s,y:.:t) -> unif ((’B’,x):bvs) (th,(s,if x==y then telse rename x y t))(s,t)-> cases bvs th (s,t)
cases bvs th (s,t) = case (strip s,strip t) of((W _F,ym),(W _G,zn)) -> flexflex bvs (_F,ym,_G,zn,th)((W _F,ym),_)-> flexrigid bvs (_F,ym,t,th)(_,(W _F,ym))-> flexrigid bvs (_F,ym,s,th)((a,sm),(b,tn))-> rigidrigid bvs (a,sm,b,tn,th)

13

Example: Computation Rules on Sum types

caseinl: a1 + a2 , (a1 → c), (a2 → c) → c: a1 → a1 + a2
inr : a2 → a1 + a2

(caseL) case(inl(X), F, G)(caseR) case(inr(Y ), F, G)(sumEta) case(Z, λx.H[inl(x)], λy.H[inr(y)])⇒ F (X)⇒ G(Y )⇒ H[Z]

14Conclusion
B Report here that FCU uniﬁcation can be implemented functionally
B SOL: Haskell-based tool for analysing conﬂuence and terminationof second-order computatoin rules– HO version of Knuth and Bendix’s critical pair checking
using FCU uniﬁcation