×

zbMATH — the first resource for mathematics

Nominal logic, a first order theory of names and binding. (English) Zbl 1056.03014
Summary: This paper formalises within first-order logic some common practices in computer science to do with representing and reasoning about syntactical structures involving lexically scoped binding constructs. It introduces Nominal Logic, a version of first-order many-sorted logic with equality containing primitives for renaming via name-swapping, for freshness of names, and for name-binding. Its axioms express properties of these constructs satisfied by the FM-sets model of syntax involving binding, which was recently introduced by the author and M. J. Gabbay and makes use of the Fraenkel-Mostowski permutation model of set theory. Nominal Logic serves as a vehicle for making two general points. First, name-swapping has much nicer logical properties than more general, non-bijective forms of renaming while at the same time providing a sufficient foundation for a theory of structural induction/recursion for syntax modulo \(\alpha\)-equivalence. Secondly, it is useful for the practice of operational semantics to make explicit the equivariance property of assertions about syntax – namely that their validity is invariant under name-swapping.

MSC:
03B70 Logic in computer science
68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
68Q55 Semantics in the theory of computing
Software:
SLMC; Coq; Isabelle
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Barendregt, H.P., The lambda calculus: its syntax and semantics, (1984), North-Holland Amsterdam · Zbl 0551.03007
[2] M.J. Beeson, Foundations of Constructive Mathematics, Ergebnisse der Mathematik und ihrer Grenzgebeite, Springer, Berlin, 1985
[3] Caires, L.; Cardelli, L., A spatial logic for concurrency (part I), (), 1-38 · Zbl 1087.03507
[4] Caires, L.; Cardelli, L., A spatial logic for concurrency (part II), () · Zbl 1012.68122
[5] Cardelli, L.; Gordon, A.D., Logical properties of name restriction, () · Zbl 0981.68036
[6] The Coq proof assistant, version 7.2, January 2002. Institut National de Recherche en Informatique et en Automatique, France. Available from <coq.inria.fr>
[7] de Bruijn, N.G., Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the church-rosser theorem, Indag. math., 34, 381-392, (1972) · Zbl 0253.68007
[8] Despeyroux, J.; Pfenning, F.; Schürmann, C., Primitive recursion for higher-order abstract syntax, (), 147-163 · Zbl 1063.03511
[9] G. Dowek, T. Hardin, C. Kirchner. A completeness theorem for an extension of first-order logic with binders, in: S. Ambler, R. Crole, A. Momigliano (Eds.), Mechanized Reasoning about Languages with Variable Binding (MERLIN 20001), Proceedings of a Workshop held in conjunction with the International Joint Conference on Automated Reasoning, IJCAR 2001, Siena, June 2001, Department of Computer Science Technical Report 2001/26, University of Leicester, 2001, pp. 49-63
[10] Dowek, G.; Hardin, T.; Kirchner, C., HOL-λσ: an intentional first-order expression of higher-order logic, Mathematical structures in computer science, 11, 1, 21-45, (2001) · Zbl 0972.03012
[11] Fiore, M.P.; Plotkin, G.D.; Turi, D., Abstract syntax and variable binding, (), 193-202
[12] Freyd, P.J., The axiom of choice, Journal of pure and applied algebra, 19, 103-125, (1980) · Zbl 0446.03042
[13] M.J. Gabbay, A theory of inductive definitions with α-equivalence: semantics, implementation, programming language, Ph.D. thesis, University of Cambridge, 2000
[14] M.J. Gabbay, FM-HOL, a higher-order theory of names, in: Thirty Five years of Automath, Heriot-Watt University, Edinburgh, April 2002, Informal Proceedings, 2002
[15] M.J. Gabbay, FM techniques in Isabelle, Preprint, March 2002
[16] Gabbay, M.J.; Pitts, A.M., A new approach to abstract syntax involving binders, (), 214-224
[17] Gabbay, M.J.; Pitts, A.M., A new approach to abstract syntax with variable binding, Formal aspects of computing, 13, 341-363, (2002) · Zbl 1001.68083
[18] Gordon, A.D.; Melham, T., Five axioms of alpha-conversion, (), 173-191
[19] Gunter, C.A., ()
[20] Hallnäs, L., Partial inductive definitions, Theoretical computer science, 87, 115-142, (1991) · Zbl 0770.68039
[21] Hamana, M., A logic programming language based on binding algebras, (), 243-262 · Zbl 1087.68529
[22] Honda, K., Elementary structures in process theory (1): sets with renaming, Mathematical structures in computer science, 10, 617-663, (2000) · Zbl 0968.68112
[23] Honsell, F.; Miculan, M.; Scagnetto, I., An axiomatic approach to metareasoning on nominal algebras in hoas, (), 963-978 · Zbl 0986.68016
[24] Huppert, B., ()
[25] Jech, T.J., About the axiom of choice, (), 345-370
[26] Makkai, M.; Reyes, G.E., First order categorical logic, Lecture notes in mathematics, vol. 611, (1977), Springer Berlin
[27] McDowell, R.C.; Miller, D.A., Reasoning with higher-order abstract syntax in a logical framework, ACM transactions on computational logic, 3, 1, 80-136, (2002) · Zbl 1365.68164
[28] McKinna, J.; Pollack, R., Some type theory and lambda calculus formalised, Journal of automated reasoning, 23, 373-409, (1999) · Zbl 0940.03019
[29] M. Miculan. Developing (meta)theory of lambda-calculus in the theory of contexts, in: S. Ambler, R. Crole, A. Momigliano (Eds.), Mechanized Reasoning about Languages with Variable Binding (MERLIN 20001), Proceedings of a Workshop held in conjunction with the International Joint Conference on Automated Reasoning, IJCAR 2001, Siena, June 2001, Department of Computer Science Technical Report 2001/26, University of Leicester, 2001, pp. 65-81 · Zbl 1268.68050
[30] Miller, D.A., A compact representation of proofs, Studia logica, 46, 4, 347-370, (1987) · Zbl 0644.03033
[31] Paulson, L.C., ()
[32] Pfenning, F.; Elliott, C., Higher-order abstract syntax, (), 199-208
[33] Pitts, A.M., Categorical logic, (), (Chapter 2) · Zbl 0521.03051
[34] Pitts, A.M., Nominal logic: A first order theory of names and binding, (), 219-242 · Zbl 1087.03510
[35] Pitts, A.M.; Gabbay, M.J., A metalanguage for programming with bound names modulo renaming, (), 230-255 · Zbl 0963.68502
[36] C. Schürmann, Automating the meta-theory of deductive systems, Ph.D. thesis, Carnegie-Mellon University, 2000
[37] Scott, D.S., Identity and existence in intuitionistic logic, (), 660-696
[38] Vestergaard, R.; Brotherson, J., A formalised first-order confluence proof for the λ-calculus using one-sorted variable names, (), 306-321 · Zbl 0981.68026
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.