zbMATH — the first resource for mathematics

Nominal unification. (English) Zbl 1078.68140
Summary: We present a generalisation of first-order unification to the practically important case of equations between terms involving binding operations. A substitution of terms for variables solves such an equation if it makes the equated terms $$\alpha$$-equivalent, i.e. equal up to renaming bound names. For the applications we have in mind, we must consider the simple, textual form of substitution in which names occurring in terms may be captured within the scope of binders upon substitution. We are able to take a “nominal” approach to binding in which bound entities are explicitly named (rather than using nameless, de Bruijn-style representations) and yet get a version of this form of substitution that respects $$\alpha$$-equivalence and possesses good algorithmic properties. We achieve this by adapting two existing ideas. The first one is terms involving explicit substitutions of names for names, except that here we only use explicit permutations (bijective substitutions). The second one is that the unification algorithm should solve not only equational problems, but also problems about the freshness of names for terms. There is a simple generalisation of classical first-order unification problems to this setting which retains the latter’s pleasant properties: unification problems involving $$\alpha$$-equivalence and freshness are decidable; and solvable problems possess most general solutions.

MSC:
 68T15 Theorem proving (deduction, resolution, etc.) (MSC2010) 03B35 Mechanization of proofs and logical operations
Software:
Freshml; ML; Qu-Prolog; SLMC
Full Text:
References:
 [1] Baader, F.; Nipkow, T., Term rewriting and all that, (1998), Cambridge University Press Cambridge [2] Barendregt, H.P., The lambda calculus: its syntax and semantics, (1984), North-Holland Amsterdam · Zbl 0551.03007 [3] L. Caires, L. Cardelli, A spatial logic for concurrency (part II), in: L. Brim, P. Janc̆ar, M. Kr̆etı́nský, A. Kuc̆era (Eds.), CONCUR 2002—Concurrency Theory, Proc. 13th Internat. Conf., Brno, Czech Republic, August 20-23, 2002, Lecture Notes in Computer Science, Vol. 2421, Springer, Berlin, 2002, pp. 209-225. · Zbl 1012.68122 [4] L. Cardelli, P. Gardner, G. Ghelli, Manipulating trees with hidden labels, in: A.D. Gordon (Ed.), Foundations of Software Science and Computation Structures, Proc. 6th Internat. Conf., FOSSACS 2003, Warsaw, Poland, Lecture Notes in Computer Science, Vol. 2620, Springer, Berlin, 2003, pp. 216-232. · Zbl 1029.68092 [5] J. Cheney, C. Urban, αProlog, a fresh approach to logic programming modulo α-equivalence, in: J. Levy, M. Kohlhase, J. Niehren, M. Villaret (Eds.), Proc. of UNIF 2003, no. DSIC-II/12/03 in Departamento de Sistemas Informáticos y Computación Technical Report Series, Universidad Politécnica de Valencia, 2003, pp. 15-19. [6] G. Dowek, Higher-order unification and matching, in: A. Robinson, A. Voronkov (Eds.), Handbook of Automated Reasoning, North-Holland, Amsterdam, 2001, pp. 1009-1062 (Chapter 16). · Zbl 1011.03005 [7] G. Dowek, T. Hardin, C. Kirchner, Higher-order unification via explicit substitutions, in: 10th Annual Symp. on Logic in Computer Science, IEEE Computer Society Press, Washington, 1995, pp. 366-374. · Zbl 1005.03016 [8] G. Dowek, T. Hardin, C. Kirchner, F. Pfenning, Higher-order unification via explicit substitutions: the case of higher-order patterns, in: Proc. of JICSLP, 1996, pp. 259-273. [9] M.P. Fiore, G.D. Plotkin, D. Turi, Abstract syntax and variable binding, in: 14th Annual Symp. on Logic in Computer Science, IEEE Computer Society Press, Washington, 1999, pp. 193-202. [10] M. Gabbay, J. Cheney, A proof theory for nominal logic, in: Nineteenth Annual IEEE Symp. on Logic in Computer Science, IEEE Computer Society Press, Washington, 2004. [11] Gabbay, M.J.; Pitts, A.M., A new approach to abstract syntax with variable binding, Formal aspects of comput., 13, 341-363, (2002) · Zbl 1001.68083 [12] Gunter, C.A., Semantics of programming languages: structures and techniques, foundations of computing, (1992), MIT Press Cambridge [13] M. Hamana, A logic programming language based on binding algebras, in: N. Kobayashi, B.C. Pierce (Eds.), Theoretical Aspects of Computer Software, Proc. 4th Internat. Symp., TACS 2001, Sendai, Japan, October 29-31, 2001, Lecture Notes in Computer Science, Vol. 2215, Springer, Berlin, 2001, pp. 243-262. · Zbl 1087.68529 [14] M. Hamana, Simple β0-unification for terms with context holes, in: C. Ringeissen, C. Tinelli, R. Treinen, R.M. Verma (Eds.), Proc. of UNIF 2002, 2002, unpublished proceedings. [15] Hashimoto, M.; Ohori, A., A typed context calculus, Theoret. comput. sci., 266, 249-271, (2001) · Zbl 0989.68017 [16] F. Honsell, M. Miculan, I. Scagnetto, An axiomatic approach to metareasoning on nominal algebras in HOAS, in: F. Orejas, P.G. Spirakis, J. Leeuwen (Eds.), Proc. 28th Internat. Colloq. on Automata, Languages and Programming, ICALP 2001, Crete, Greece, July 2001, Lecture Notes in Computer Science, Vol. 2076, Springer, Heidelberg, 2001, pp. 963-978. · Zbl 0986.68016 [17] J.W. Klop, Term rewriting systems, in: S. Abramsky, D.M. Gabbay, T.S.E. Maibaum (Eds.), Handbook of Logic in Computer Science, Vol. 2, Oxford Univercity Press, Oxford, 1992, pp. 1-116. [18] Martelli, A.; Montanari, U., An efficient unification algorithm, ACM trans. programming languages and syst., 4, 2, 258-282, (1982) · Zbl 0478.68093 [19] S. Michaylov, F. Pfenning, An empirical study of the runtime behaviour of higher-order logic programs, in: D. Miller (Ed.), Proc. Workshop on the λProlog Programming Language, University of Pennsylvania, 1992, pp. 257-271, CIS Technical Report MS-CIS-92-86. [20] Miller, D., A logic programming language with lambda-abstraction, function variables, and simple unification, J. logic and comput., 1, 497-536, (1991) · Zbl 0738.68016 [21] Milner, R.; Parrow, J.; Walker, D., A calculus of mobile processes (parts I and II), Inform. and comput., 100, 1-77, (1992) [22] Milner, R.; Tofte, M.; Harper, R.; MacQueen, D., The definition of standard ML (revised), (1997), MIT Press Cambridge [23] Nickolas, P.; Robinson, P.J., The qu-prolog unification algorithmformalisation and correctness, Theoret. comput. sci., 169, 81-112, (1996) · Zbl 0874.68134 [24] R. Paterson, Unification of schemes of quantified terms, in: Proc. of UNIF 1990, 1990, unpublished proceedings. [25] Paterson, M.S.; Wegman, M.N., Linear unification, J. comput. syst. sci., 16, 2, 158-167, (1978) · Zbl 0371.68013 [26] F. Pfenning, C. Elliott, Higher-order abstract syntax, in: Proc. ACM-SIGPLAN Conf. Programming Language Design and Implementation, ACM Press, New York, 1988, pp. 199-208. [27] Pitts, A.M., Nominal logic, a first order theory of names and binding, Inform. and comput., 186, 165-193, (2003) · Zbl 1056.03014 [28] G.D. Plotkin, An illustrative theory of relations, in: R. Cooper, Mukai, J. Perry (Eds.), Situation Theory and its Applications, CSLI Lecture Notes, Vol. 22, Stanford University, 1990, pp.133-146. [29] Qian, Z., Unification of higher-order patterns in linear time and space, J. logic and comput., 6, 3, 315-341, (1996) · Zbl 0863.68074 [30] Salibra, A., On the algebraic models of lambda calculus, Theoret. comput. sci., 249, 197-240, (2000) · Zbl 0949.68048 [31] Sato, M.; Sakurai, T.; Kameyama, Y., A simply typed context calculus with first-class environments, J. funct. logic programming, 4, (2002) · Zbl 1037.68040 [32] Sato, M.; Sakurai, T.; Kameyama, Y.; Igarashi, A., Calculi of meta-variables, (), 484-497 · Zbl 1116.03321 [33] M.R. Shinwell, A.M. Pitts, M.J. Gabbay, FreshML: programming with binders made simple, in: Eighth ACM SIGPLAN Internat. Conf. on Functional Programming (ICFP 2003), Uppsala, Sweden, ACM Press, New York, 2003, pp. 263-274. · Zbl 1315.68058 [34] Urban, C.; Pitts, A.M.; Gabbay, M.J., Nominal unification, (), 513-527 · Zbl 1116.03322
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.