In A Larger Decidable Semiuniï¬cation Problem(2007), Brad Lushman and Gordon V. Cormack of University of Waterloo

[...] present a graph-theoretic framework in which to study instances of the semiunification problem (SUP), which is known to be undecidable, but has several known and important decidable subsets. One such subset, the acyclic semiunification problem (ASUP), has proved useful in the study of polymorphic type inference. We present graph-theoretic criteria in our framework that exactly characterize the ASUP acyclicity constraint. We then use our framework to find a decidable subset of SUP (which we call R-ASUP), which has a more natural description than ASUP, and strictly contains it.

## Recent comments

1 day 6 hours ago

1 day 10 hours ago

3 days 4 hours ago

3 days 5 hours ago

3 days 12 hours ago

3 days 14 hours ago

3 days 22 hours ago

3 days 22 hours ago

3 days 22 hours ago

4 days 30 min ago