typing in ML+

To: types@theory.lcs.mit.edu
Subject: typing in ML+
From: kfoury%bu-cs.bu.edu@bu-it.BU.EDU
Date: Fri, 20 May 88 19:00:09 EDT
Cc: kfoury@bu-cs.bu.edu
Announcement concerning:

"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: kfoury@bu-cs.bu.edu) 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)
defined by:

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