Lucilia Figueiredo Semi-unification

SEMI-UNIFICATION and Periodicity of Turing Machines

People:  Carlos Camarão  (DCC-UFMG)

Lucilia Figueiredo (DECOM-UFOP)

# The Semi-unification problem:

The semi-unification problem can be stated as follows:

Let Σ be an alphabet with a single function symbol, say –› (written in infix notation, as usual). Let also V be a countably infinite set of variables (denoted by a, b, c, d, e). Let T be the set of terms (denoted by t, u) over Σ and V.

Given a pair of inequalities  Γ = (tu, t'u'), — called an instance of SUP — a triple (S,S_0, S_1) of substitutions is a solution of  Γ whenever S_0(S(t)) = S(u) and S_1(S(t')) = S(u').

The semi-unification problem over an alphabet Σ is the problem of determining whether a given Γ has a solution.

The substitution S in a solution (S, S_0, S_1) of Γ is called a semi-unifier of Γ, and S_0,S_1 the corresponding residual substitutions.

# Motivation:

Our main motivation for studying the semi-unification problem has been its equivalence to the problem of typability in the Milner-Mycroft type system [6] (proofs of this equivalence can be found in [2,3]). The Milner-Mycroft calculus generalizes the Damas-Milner calculus [5]. The latter encodes the ability of let-bound variables to be used with different types in different program contexts, each of these types an instance of a most general (or principal) type; this ability is the characteristic property of parametric polymorphism, explored in languages such as ML and Haskell. The Milner-Mycroft calculus provides a more general rule for recursive definitions, which allows a variable to be used polymorphically inside its own definition (called polymorphic recursion).

# Results:

The undecidability of the semi-unification problem SUP has been proved, by Kfoury, Tiuryn and Urzyczyn [2], by a reduction to the boundedness problem for Turing Machines. The proof is based on constructing, for any given symmetric intercell Turing Machine (SITM) M, an instance Γ of SUP such that M is bounded if and only if Γ has a solution.

Fritz Henglein simultaneously presented [4] a rewriting system for semi-unification, for which no example was known that caused the rewriting system to loop forever.

We have defined a rewriting system RSUP [5] that is proved to be equivalent to Henglein’s rewriting system and also defined a  converse mapping I(Γ) from instances of SUP Γ into intercell Turing Machines and proved that, for any instance of SUP Γ:

• RSUP terminates indicating that Γ has a solution if and only if I(Γ) is bounded (analogously to the proof in [2])
• if RSUP terminates indicating that  Γ has no solution, then I(Γ) has an eventually periodic configuration
• if RSUP does not terminate with input Γ, then I(Γ) has a wandering (neither halting nor eventually periodic) configuration.

Based on these results, we were able to present an example for which RSUP and Henglein’s HRS do not terminate. The example – named K2 – is taken from a recent work on the existence of non-periodic configurations of Turing Machines with no halting configuration, by Blondel, Cassaigne and Nichitiu [1].

Given that wandering configurations seem to occur rarely in practice (let alone on TMs constructed out of instantiations

of polymorphic types), we expect that polymorphic recursion can be used in practice without significant problems and constitute a useful feature in programming languages.

# Software and examples:

tm2itm: Haskell source code for converting a Turing Machine to Intercell Turing Machine

itm2sup: Haskell source code for converting the right (or left) moves of the symmetric closure of an Intercell Turing Machine to an instance of the semi-unification problem

rsup: Haskell source code for running our rewriting system RSUP on instances of the semi-unification problem.

Examples:

K2.tm: An example, from [1], of a Turing Machine with no periodic and no halting configuration

K2.itm: An equivalent Intercell Turing Machine

K2.in: An instance of the semi-unification problem "corresponding" to the symmetric closure of K2.itm

Robert Staerk’s semiunif-1.0:  An implementation of Henglein’s algorithm

Type Inference for polymorphic recursion:

Here is our prototype implementation of type inference for polymorphic recursion, for a Haskell-like language, without overloading. The type inference is based on the ideas of RSUP and on Mark Jones’s type inference algorithm for Haskell. Here are some examples for experimenting with our type inference prototype.

The implementation is described in the following paper: Practical Type Inference for Polymorphic Recursion: an Implementation in Haskell (ps.gz), Cristiano VasconcelosLucília Figueiredo, Carlos Camarão, Proceedings of SBLP'2003 - VII Brasilian Symposium on Programming Languages, Ouro Preto, MG, Brasil, May 2003, in Journal of Universal Computer Science, volume 9(8), 2003. Also available at http://www.jucs.org/jucs_9_8/7th_brasilian_symposium_on.

An implementation of a type inference algorithm for overloading and polymorphic recursion, based on RSUP is available at http://www.dcc.ufmg.br/~camarao/CT

# Bibliography:

[1] On the presence of periodic confiurations in Turing Machines and in counter machines. Blondel, V., Cassaigne, J. and Nichitiu, C., TCS 289, p. 573-590, 2002.

[2] The undecidability of  the semi-unification problem, Kfoury, A, Tiuryn, J. and Urzyczyn, P. Information and Computation 1, p.83-101, 1993.

[3] Type reconstruction in the presence of polymorphic recursion, Kfoury, Tyurin, Urzyckyn, ACM TOPLAS 15(2),  1993, p. 290 - 311

[4] Type inference with polymorphic recursion. Henglein, F., ACM TOPLAS 15, p. 253-289, 1993.

[5] Semi-unification and Periodicity of Turing Machines (.ps). Lucília Figueiredo and Carlos Camarão, draft (to be submitted).

[6] A theory of type polymorphism in programming. Milner, R., Journal of Computer and System Sciences 17, p. 348-375, 1978.

[7] Polymorphic type schemes and recursive definitions. Mycroft, A., Proceedings of the International Symposium on Programming, LNCS 167, p. 217-239, 1984.