typing in ML+
"A Proper Extension of ML with an Effective Type Assignment"
by A.J. Kfoury, J. Tiuryn, and P. Urzyczyn,
in Proceedings of POPL '88.
In the above mentioned report we propose a cut-and-paste
technique to decide whether an expression has a typing
in ML+ . We have discovered a gap in our proof that this
algorithm is correct. We are presently working on filling
the gap. In the meantime we have formulated a Generalized
Unification Problem (GUP) to which the ML+ typing problem
is reducible. The decidability of GUP implies the decidability
of typing in ML+.
We give below a precise statement of GUP. A draft of the
proof of the reduction to GUP will be available from Dennis
(internet: email@example.com) by June 1. Comments on the
problem and new ideas for solving it (more simply than our
cut-and-paste method) are most welcome.
A GENERALIZED UNIFICATION PROBLEM
T(X) is the set of first-order terms over an infinite set of
variables, X, and a signature containing exactly one binary
function symbol and an arbitrary number of constant symbols.
A substitution S is a mapping from X to T(X) such that S(x) = x
for all but finitely many x in X. Extending S to any t in T(X),
S(t) is the result of replacing each variable x in t by S(x).
D(X) is the free distributive lattice generated by X, with bottom
element, top element, glb and lub.
P(X) is the powerset of X, which is also a distributive lattice
with bottom element (empty set) and top element X.
Viewing a substitution S: T(X) --> T(X) as a homomorphism on the
term algebra T(X), S induces a lattice homomorphism S~: D(X) --> P(X)
S~(x) = the set of variables in S(x)
for every generator x in X, which lifts in the obvious way to
every d in D(X).
Let t, u in T(X) and d in D(X). We say that the substitution
S: T(X) --> T(X) satisfies the inequation (t,d) <= u iff
there exists a substitution R: T(X) --> T(X) such that:
(1) R(x) = x for every x in S~(d), and
(2) R(S(t)) = S(u).
An instance I of GUP is a finite (non-empty) set of inequations
each of the form (t,d) <= u.
The problem is: Is it decidable, for an arbitrary instance I of GUP,
whether there is a substitution satisfying every inequation in I ?
Remark: In the special case when d = T (the top element in the lattice
D(X)), the substitution S satisfies the inequation (t,d) <= u iff
S(t) = S(u). Thus, when d = T in all inequations of instance I, I
reduces to an instance of the standard (first-order) unification