zbMATH — the first resource for mathematics

The Qu-Prolog unification algorithm: formalisation and correctness. (English) Zbl 0874.68134
Summary: Qu-Prolog is an extension of Prolog which performs meta-level computations over object languages, such as predicate calculi and \(\lambda\)-calculi, which have object-level variables, and quantifier or binding symbols creating local scopes for those variables. As in Prolog, the instantiable (meta-level) variables of Qu-Prolog range over object-level terms, and in addition other Qu-Prolog syntax denotes the various components of the object-level syntax, including object-level variables. Further, the meta-level operation of substitution into object-level terms is directly represented by appropriate Qu-Prolog syntax. Again as in Prolog, the driving mechanism in Qu-Prolog computation is a form of unification, but this is substantially more complex than for Prolog because of Qu-Prolog’s greater generality, and especially because substitution operations are evaluated during unification. The Qu-Prolog unification algorithm is specified, formalised and proved correct. Further, the analysis of the algorithm is carried out in a framework which straightforwardly allows the ‘completeness’ of the algorithm to be proved: though fully explicit answers to unification problems are not always provided, no information is lost in the unification process.

68W10 Parallel algorithms in computer science
Full Text: DOI
[1] Cheng, A.S.K.; Robinson, P.J.; Staples, J., Higher level meta programming in qu-prolog 3.0, (), 285-298
[2] de Bruijn, N.G., Lambda calculus notation with nameless dummies, Nederl. akad. wetensch. series A, 75, 381-392, (1972) · Zbl 0253.68007
[3] Huet, G.P., A unification algorithm for typed λ-calculus, Theoret. comput. sci., 1, 27-57, (1975) · Zbl 0337.68027
[4] Lloyd, J.W., Foundations of logic programming, (1987), Springer Berlin, New York · Zbl 0547.68005
[5] Mendelson, E., Introduction to mathematical logic, (1987), Wadsworth and Brooks/Cole CA · Zbl 0192.01901
[6] Nadathur, G.; Miller, D., An overview of λprolog, (), 810-827
[7] G. Nadathur and D. Miller, Higher-order logic programming, in: D. Gabbay, C. Hogger and A. Robinson, eds., Handbook of Logic in Artificial Intelligence and Logic Programming (Oxford University Press, to appear). · Zbl 0900.68129
[8] Paterson, R., Unification of schemes of quantified terms, ()
[9] Paterson, R.A.; Staples, J., Unification and constraint solution for metaprogramming: an overview, (), 367-380
[10] Robinson, P.J.; Cheng, A., Technical report no. 93-18, ()
[11] Staples, J.; Robinson, P.J.; Paterson, R.A.; Hagen, R.A.; Craddock, A.J.; Wallis, P.C., Qu-prolog: an extended prolog for meta level programming, (), 435-452
[12] Stoughton, A., Substitution revisited, Theoret. comput. sci., 59, 317-325, (1988) · Zbl 0651.03008
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.