|
|
|
|
SEMI-UNIFICATION and
Periodicity of Turing Machines
|
|
People:
Carlos
Camarão (DCC-UFMG)
Lucilia
Figueiredo (DECOM-UFOP)
Cristiano Damiani
Vasconcelos (PucPR)
|
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 Γ
= (t ≤ u, 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 http://www.cis.uni-munchen.de/~leiss/polyrec.html
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 Vasconcelos, Lucí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.
|
|
|
