×
Urban, Christian; Pitts, Andrew M.; Gabbay, Murdoch J.

Nominal unification. (English) Zbl 1078.68140

Theor. Comput. Sci. 323, No. 1-3, 473-497 (2004).
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.

Cited in 2 Reviews
Cited in 67 Documents

MSC:

68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
03B35 Mechanization of proofs and logical operations

Keywords:

Abstract syntax; Alpha-conversion; Binding operations; Unification

Software:

SLMC; ML; Freshml; Qu-Prolog
PDFBibTeX XMLCite
\textit{C. Urban} et al., Theor. Comput. Sci. 323, No. 1--3, 473--497 (2004; Zbl 1078.68140)
Full Text: DOI

References:

[1] Baader, F.; Nipkow, T., Term Rewriting and All That (1998), Cambridge University Press: Cambridge University Press Cambridge
[2] Barendregt, H. P., The Lambda Calculus: Its Syntax and Semantics (1984), North-Holland: 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.; 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.; 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, \(αα\); J. Cheney, C. Urban, \(αα\)
[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).; 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.; 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.; 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.; 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.; 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: MIT Press Cambridge · Zbl 0823.68059
[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.; 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\); M. Hamana, Simple \(β_0\)
[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.; 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.; 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. · Zbl 0777.68001
[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 \(λ\); S. Michaylov, F. Pfenning, An empirical study of the runtime behaviour of higher-order logic programs, in: D. Miller (Ed.), Proc. Workshop on the \(λ\)
[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) · Zbl 0752.68037
[22] Milner, R.; Tofte, M.; Harper, R.; MacQueen, D., The Definition of Standard ML (Revised) (1997), MIT Press: 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.; 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.; 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.; 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. · Zbl 0942.03521
[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, (Baaz, M., Proc. Comput. Sci. Logic and 8th Kurt Gödel Colloq. (CSL’03 & KGC), Vienna, Austria. Proc. Comput. Sci. Logic and 8th Kurt Gödel Colloq. (CSL’03 & KGC), Vienna, Austria, Lecture Notes in Computer Science, Vol. 2803 (2003), Springer: Springer Berlin), 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.; 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, (Baaz, M., Proc. Comput. Sci. Logic and 8th Kurt Gödel Colloq. (CSL’03 & KGC), Vienna, Austria. Proc. Comput. Sci. Logic and 8th Kurt Gödel Colloq. (CSL’03 & KGC), Vienna, Austria, Lecture Notes in Computer Science, Vol. 2803 (2003), Springer: Springer Berlin), 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. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.