A Functional Implementation of
Function-as-Constructor Higher-Order Uniﬁcation
Makoto Hamana1
Department of Computer Science, Gunma University, Japan
hamana@cs.gunma-u.ac.jp
Abstract
Recently, Libal and Miller showed a new decidable class of higher-order uniﬁcation
problems called Functions-as-Constructors uniﬁcation (FCU). It extends the class of higherorder patterns and retains good properties of pattern uniﬁcation. But no implementation of
FCU uniﬁcation has been given. We report here that FCU uniﬁcation can be implemented
nicely functionally. We have implemented the FCU uniﬁcation in Haskell as a part of oursystem SOL, Second-Order Laboratory, for critical pair checking of higher-order rules. Our
experience on SOL system analysing various computation rules in programming languages
shows that the functional FCU uniﬁcation is useful in practice.

1

Introduction

It is widely known that Miller’s higher-order patterns provide a decidable class of higher-order
uniﬁcation [Mil91]. These have been used as the basic term structure for pattern matchingin various computational systems, such as higher-order logic programming [Mil91] and rewrite
rules [MN98]. Higher-order patterns have nice properties: there exists the most general uniﬁer(mgu) for a solvable uniﬁcation problem, and an eﬃcient algorithm is known [Bax77]. However,the class is a bit restrictive in practice.
Consider the following example. Suppose a simple type system having sum types a + b andthe function symbols case : a1 + a2 , (a1 → c), (a2 → c) → c for case-construct and inl : a1 →
a1 + a2 , inr : a2 → a1 + a2 for inclusions. Consider the computation rules on sum types(caseL) case(inl(X), F, G)⇒ F (X)(caseR) case(inr(Y ), F, G)⇒ G(Y )
(sumEta) case(Z, λx.H[inl(x)], λy.H[inr(y)]) ⇒ H[Z]In this paper, we use the notation M [t1 , . . . , tn ] to denote a λ-term of application
M t1 · · · tn with a free variable M . The rules (caseL) and (caseR) deﬁne the computation
behavior of the case-construct. The rule (sumEta) is the η-reduction rule of case-expression.
An important fact is that λx.H[inl(x)] and λy.H[inr(y)] are not higher-order patterns.
A higher-order pattern is a term where every application is of the form M [x1 , . . . , xn ], i.e.
a free variable M must be applied to distinct bound variables x1 , . . . , xn . Therefore, terms
such as M [N ], M [cons(x, y)], λx.H[inl(x)], λy.H[inr(y)] are not higher-order patterns. Hence,the existing algorithm for higher-order pattern matching cannot be used for computing with arule such as (sumEta). This is problematic for general higher-order computation. Moreover,it means that we cannot compute overlapping between rules to compute critical pairs for local
conﬂuence [KB70]. It needs uniﬁcation between the left-hand sides of rules of this kind of
higher-order rules. However, the existing higher-order pattern uniﬁcation cannot cope with theterms λx.H[inl(x)] and λy.H[inr(y)].
Recently, Libal and Miller present a new decidable class of higher-order uniﬁcation problems
called Functions-as-Constructors uniﬁcation (FCU) [LM16]. It extends the class of higher-orderA Functional Implementation of Function-as-Constructor Higher-Order Uniﬁcation

Makoto Hamana

pattern uniﬁcation and retains good properties of pattern uniﬁcation, namely, it ensures theexistence of the most general uniﬁer if an FCU problem is uniﬁable. Interestingly, it can solve
the above mentioned problem. Terms such as λx.H[inl(x)] and λy.H[inr(y)] can be targets of
FCU uniﬁcation. Hence, we have recoginised that FCU uniﬁcation is useful to formulate a new
eﬀective class for higher-order computation [Ham17].
In this paper, we report that FCU uniﬁcation can be implemented functionally. In [LM16],
Libal and Miller gave an algorithm for FCU uniﬁcation, but they did not provide its implementation. They mentioned that the implementation is a further work. We have implemented the
FCU uniﬁcation algorithm and its slight extension in Haskell, which has been a part of the SOL
system for critical pair checking of computation rules [Ham17]. Our experience on SOL systemanalysing various computation rules in programming languages shows that the functional FCU
uniﬁcation is useful in practice.

2

FC patterns and matching

We ﬁrst introduce the notion of FC patterns and matching. We denote by s £ t if s is a subtermof t, and s ¢ t if s £ t and s 6= t. We use the notation A for a sequence A1 , · · · , An .
An FC pattern is a term p in which every occurrence of application M [t1 , . . . , tn ] in p, thefollowing conditions are satisﬁed:(i) every ti is a term without binders, metavariables or free variables, but it can containfunction symbols with arity n > 0 and bound variables(ii) every ti contains at least one bound variable,(iii) ti £6 tj for every 1 ≤ i, j ≤ n.
For example, M [cons(x, y)] is an FC pattern. FC patterns extend Miller’s higher-orderpatterns, because “metavariables with distinct bound variables” are ensured by (ii)(iii). A?

matching problem s = t is an equation consisting of terms s, t, both of which are in long β
η-normal forms. It asks whether there exists a matcher θ such that s θ = t holds. A uniﬁcation?
problem s = t is an equation consisting higher-order patterns s, t in long β η-normal forms. It
asks whether there exists a uniﬁer θ such that s θ = t θ holds.
?

Theorem 2.1. ([YHT04a]) Any second-order FC pattern matching problem p = t between
an FU pattern p and a λ-term t is decidable and has a single most general matcher if matchable.
?

What about uniﬁcation? In contrast to matching, uniﬁcation problem p = t between FC
patterns may not have a single most general uniﬁer. Yokoyama et al. [YHT04b, Sec. 2] haveshown such an example. 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}. FCU uniﬁcation avoids this problem by identifying such a kind of problems.

3

FCU uniﬁcation

Libal and Miller’s Functions-as-Constructors Uniﬁcation (FCU) [LM16] imposes an additional?

restriction to a uniﬁcation problem in order to ensure the existence of mgu. A problem s = t is2

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

?

Q∀

(abs)

Q∀

(fun)

t=t

λx.s = λx.t →?

Q∀(ﬂex-rigid)

→

?

Q∀
x, Q∀

→

Q∀

F t=f s →Q∀f s=f t?

Q∀

Makoto Hamana

∅

[]
?

∅

s=t
?

?

∅

s1 = t1 , . . . , sn = tn[] {F 7→ λz.discharge (zip t z) (f s)}?

{X 7→ λz1 , . . . , zn .Hz 0 }(ﬂex-ﬂex same)Q∀

F t=F s →Q∀[]
where z 0 = (zi | 1 ≤ i ≤ n, ti = si )(ﬂex-ﬂex diﬀ)

Q∀

F t=Gs →Q∀ s = t{Y 7→ λz1 , . . . , zm .Hzϕ(i) },where ϕ(j) = i if ti = sj for i = 1, . . . , n, j = 1, . . . , m.

?

?

Figure 1: An FCU uniﬁcation algorithm
called FCU uniﬁcation if s and t are FC patterns and satisﬁes the following condition ([LM16,
Def. 14]).
?

• Global restriction: in s = t, for every two diﬀerent occurrences of applications M [s1 , . . . , sn ]and N [t1 , . . . , tm ], si ¢6 tj holds for every 1 ≤ i ≤ n, 1 ≤ j ≤ m.
Note that Yokoyama et al.’s example actually violates the global restriction.
Theorem 3.1. ([LM16]) An FCU uniﬁcation problem is decidable and ensures the existenceof a most general uniﬁer if solvable.

3.1

Functional FCU uniﬁcation

An FCU uniﬁcation algorithm has been given in [LM16], which is shown to be terminating andreturns a most general uniﬁer. But no implementation of FCU uniﬁcation has been reported in
the literature. The algorithm in [LM16] is not immediately ready for implementation, because
it requires several complex operation during uniﬁcation such as pruning and discharging.
Nipkow has given a functional formulation of pattern uniﬁcation and an ML implementation[Nip93]. Our strategy of implementing FCU is to base Nipkow’s functional implementationand to adapt it to the case of FCU. This approach is solid and realistic because Nipkow’s
implementation has given a basic library and infrastructure for higher-order uniﬁcation, suchas on-the-ﬂy α-conversion and η-expansion. Moreover, FCU was designed to be an improvementof pattern uniﬁcation.
Based on this approach, we proceed to give a functional FCU. The transformation rules inFig. 1, slightly modiﬁed from [LM16] for our functional implementation, are of the formhQ∀ , s = ti → hQ0∀ , E 0 , θ0 i?

?

which is read as follows. The uniﬁcation problem s = t has a set of free variables (or, universallyquantiﬁed by) Q∀ and it is translated to the list of uniﬁcation problems E 0 under the new
substitution θ0 . In the rule (ﬂex-rigid), the function discharge is a discharging function [YHT04a]that replaces every term t in t with a variable z in z. In the rules (ﬂex-ﬂex same/diﬀ), thevariable H is assumed to be fresh. The actual transformation relation is deﬁned by?

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

if hQ∀ , s = ti → hQ0∀ , E 0 , θi?

(1)

and apply the “pruning” operation described later if applicable. Here “:” is cons and “++ ” isthe append for lists, and (−) ↓β computes the β-normal form.
3

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

Theorem 3.2. A list of FCU uniﬁcation problems E has a solution iﬀ hE, ∅iwhich θ restricted to free variables of E is a most general uniﬁer of E.

Makoto Hamana∗- h[], θi, in

Implementation. In our implementation, we implement the rules in Fig. 1 with the actual
transformation (1). Although this division was not taken in the original FCU [LM16], this is
more handy in the functional implementation and also has been taken in the pattern uniﬁcation[Nip93].
Data structure. We deﬁne the datatype of λ-terms bydata Term = W Id

| O Id| C Id| Term :@ Term | Id :.: Term | Term :#: Term | End

where the constructor W for free variables for uniﬁcation, O for bound (and freed) variables, :@:for application, and :#: for paring with the terminal End. The construct x :.: t expresses
an abstraction λx.t. We deﬁne Id to be String.

3.2

Pruning

The pruning operation is one of the most complicated operations in FCU [LM16, Def.26]. It
prunes some uniﬁcation problem which can be solved immediately. Suppose an FCU uniﬁcation
problem hQ∀ , E, ρi such that E involves an equation of the form?

X[t] = u ¥ W [· · · , q, · · · ]where a term q is the i-th argument of m-ary free variable W , and t do not involve q. Then, thealgorithm prunes this equation and obtains the substitution W 7→ z.H[z 0 ], where z 0 is obtained
from z by deleting the i-th zi , and H is fresh. This is implemented as the function
prune t (ρ, u)
which also deals with suitable η-expansion.
prune tn (rho,u) = case strip (devar rho u) of(x:.:t’,_)-> prune (O x : tn) (rho,t’)(C _, rr) -> foldlN (prune tn) (rho,rr)(O x, rr) -> if O x ‘elem‘ tn
then foldlN (prune tn) (rho,rr) else xxFail "Not unifiable"(W _W, sm)-> if sm ‘subset‘ tn -- all sm appear in lhs
then rho else let vsm = mkvars sm_H = xxNewW "H"in (_W, hnf (vsm, _H, eqsel vsm tn sm)) : rho

Here devar ρ u applies a substitution ρ to a term u, strip splits a term as the head term andthe rest of terms, and hnf computes the head normal form, deﬁned in [Nip93]. H is a new freevariable.

3.3

Discharging operation

FCU uniﬁcation requires the operation t|sz , which Yokoyama et al. called “discharging”, that
replaces terms s in t with variables z. Yokoyama et al. gave a bit complicated algorithm forit [YHT04a]. Observing the similarity between the discharging operation and substitution ofterms for variables, we can simply implement t|sz as discharge θ t as follows.
4

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

Makoto Hamana

discharge :: [(Term, Id)] -> Term -> Termdischarge th t = case lookup t th of
Just y -> O y
Nothing -> case t of
(x :.: t1) -> x :.: discharge th t1(t1 :@ t2) -> (discharge th t1) :@ (discharge th t2)t-> tHere, lookup t th looks up a term t in an association list th.
Uniﬁcation function. Finally, we implement the transformation (1) and the dispatcher
according to the cases in Fig. 1 as the main function unif. Here, unif bvs (th,(s,t))?
means to process the uniﬁcation 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 t else 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)

For space reason, we only show the case of (ﬂex-rigid).
flexrigid bvs (_F,tn,s,rho) -- s is rigid| occ _F rho s = xxFail "Not unifiable at flex-rigid"| otherwise = let zn= mkvars tn
theta = (_F, abst (zn, discharge (zip tn zn) s))in prune bvs tn (theta:rho, discharge (zip tn zn) s)

where occ is the occur-check function.
Other cases are also implemented in this way. The interested reader is referred to theimplementation of our SOL system, which will be available from the author’s homepage.

References[Bax77][Ham17][KB70][LM16][Mil91]

L. Baxter. The complexity of uniﬁcation. PhD thesis, Department of Computer Science,
University of Waterloo, 1977.
M. Hamana. How to prove your calculus is decidable: practical applications of second-orderalgebraic theories and computation. Proceedings of the ACM on Programming Languages,
1(1):22:1–22:28, 9 2017.
D. Knuth and P. Bendix. Simple word problems in universal algebras. In Computational
Problem in abstract algebra, pages 263–297. Pergamon Press, Oxford, 1970. included alsoin Automationof reasoning 2, Springer (1983), pp.342-376.
T. Libal and D. Miller. Functions-as-Constructors Higher-Order Uniﬁcation. In Proc. of
FSCD 2016, volume 52 of Leibniz International Proceedings in Informatics (LIPIcs), pages
26:1–26:17, 2016.
D. Miller. A logic programming language with lambda-abstraction, function variables, andsimple uniﬁcation. Journal of Logic and Computation, 1(4):497–536, 1991.

5

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

Makoto Hamana

R. Mayr and T. Nipkow. Higher-order rewrite systems and their conﬂuence. Theor. Comput.
Sci., 192(1):3–29, 1998.
[Nip93]
T. Nipkow. Functional uniﬁcation of higher-order patterns. In Proc. of (LICS’93), pages
64–74, 1993.
[YHT04a] T. Yokoyama, Z. Hu, and M. Takeichi. Deterministic second-order patterns. Inf. Process.
Lett., 89(6):309–314, 2004.
[YHT04b] T. Yokoyama, Z. Hu, and M. Takeichi. Deterministic second-order patterns for programtransformation. Computer Software, 21(5):71–76, 2004. in Japanese.
[MN98]

6