Unification under associativity and idempotence is of type nullary
Tóm tắt
It is shown, that there exist a unification problem〈s=t〉
AI
, for which the set of solutions under associativity and idempotence is not empty. But
$$\mu U\sum _{Al} \left( {s,t} \right)$$
, the complete and minimal subset of this set of solutions does not exist, i.e.A+I is of type nullary. This is the first known standard first order theory with this unpleasant feature.
Tài liệu tham khảo
Fages, F and Huet, G., ‘Complete sets of unifiers and matchers in equational theories’, CAAP 83,Trees in Algebra and Programming, (eds. G. Ausiello and M. Protasi), Springer Verlag, LNCS 159, pp. 250–220, (1983).
Gould, W. E., A matching procedure for ω-order logic,Scientific Report No. 4, Air Force Cambridge Research Labs., (1966).
Howie, J. M.,An Introduction to Semigroup Theory, Academic Press, (1976).
Huet, G.,Resolution d'equations dnans des languages d'ordere 1,2, ... w, These d'Etat, Univ. de Paris, VII, (1976).
Siekmann, J. H., Universal unification, Proc. of the 7th CADE, (ed R.E. Shostak), Springer Verlag LNCS 170, pp. 1–42, (1984).
SiekmannJ. and SzabóP.A Noetherian and Confluent Rewrite System for Idempotent Semigroups Forum Vol. 25, pp. 83–110, Springer Verlag New York, (1982).
Szabó, P.,Theory of First Order Unification, (in German, thesis) Univ. Karlsruhe, 1982.