-
gabbay:stusun
-
Murdoch J. Gabbay
A study of substitution, using nominal techniques and Fraenkel-Mostowski sets.
A journal version of my AISB'08 paper, with two subtitution actions and full proofs.
We investigate two capture-avoiding substitutions action on Fraenkel-Mostowski set theory, in the sense of capasn-jv.
Substitution is commonly understood as an action on syntax (for example when building a logic or a lambda calculus) and thus as a prelude to, but not a part of, mathematical denotations.
We investigate it as an operation on a mathematical foundation, specifically, Fraenkel-Mostowski set theory.
-
gabbay:nomahs
-
Murdoch J. Gabbay
Nominal Algebra and the HSP theorem,
pending publication in the Journal of Logic and Computation.
Nominal Algebra is a version of universal algebra based on nominal terms — thus, an equivariant system with support for freshness, binding, and permutation, as promoted by me and Pitts, and later by me and Mathijssen.
The HSP theorem for universal algebra states that any algebra is the homomorphic image of subalgebra of a product of free algebras; think of this as ‘the fundamental theorem of arithmetic’ (any number is the product of prime numbers), but for algebras.
Mathematicians like to prove this kind of result; it puts a limit the number of ways that a widget can be constructed, and thus on the widget's mathematical behaviour.
In this paper we prove an HSP theorem for nominal algebra.
The twist in the tale is that we must also assume atoms-abstraction, a construct characteristic of nominal techniques.
The proofs are also rather beautiful, if you like nominal sets.
-
gabbay:alwa-jv
-
Murdoch J. Gabbay and Michael J. Gabbay
a-logic with arrows (journal version),
in ENTCS.
DOI 10.1016/j.entcs.2008.06.031.
The journal version of our WFLP'07 paper, with an improved proof-system.
a-logic has a predicate ‘atom’ which is true of a term when it is a variable symbol.
We prove cut-elimination, give a notion of model, prove soundess and completeness, and axiomatise substitution and the lambda-calculus, using ‘atom’ to identify variables.
-
gabbay:capasn-jv
-
Murdoch J. Gabbay and Aad Mathijssen
Capture-avoiding Substitution as a Nominal Algebra,
in Formal Aspects of Computing.
also available online in DOI 10.1007/s00165-007-0056-1.
We investigate capture-avoiding substitution using Nominal Algebra.
This is a journal version of a conference paper, with improved proofs.
-
gabbay:oneaah-jv
-
Murdoch J. Gabbay and Aad Mathijssen
One-and-a-halfth-order logic,
in the Journal of Logic and Computation.
DOI 10.1093/logcom/exm064.
We present a logic similar to first-order logic, but with predicate unknowns in nominal style. This permits schematic reasoning in the presence of ‘unknown predicates’ which may also occur under binders. We give both algebraic and sequent characterisations of derivability, prove their equivalence, prove cut-elimination of the sequent system, and show correctness with respect to first-order logic.
A conference version is here.
-
gabbay:nomr-jv
-
Maribel Fernandez and Murdoch J. Gabbay
Nominal Rewriting,
in Information and Computation, Volume 205, Issue 6, June 2007, Pages 917-965, DOI 10.1016/j.ic.2006.12.002.
The journal version of our PPDP'04 paper. Nominal rewriting is rewriting in the presence of meta-level unknowns, object-level variable symbols, and alpha-equivalence, but nothing else. Substitution of terms for unknowns remains first-order; no capture-avoidance.
-
gabbay:hienr
-
Murdoch J. Gabbay
Hierarchical nominal terms and their theory of rewriting,
in Electronic Notes in Theoretical Computer Science, Volume 174, Issue 5, 2 June 2007, Pages 37-52, DOI 10.1016/j.entcs.2007.01.017.
We build a theory of rewriting on nominal terms with an infinite hierarchy of ‘meta-level variables’. We use it to examine some case studies, including capture- and non-capture avoiding substitution and the NEW calculus of contexts as rewrite systems.
A workshop version appeared in proceedings of LFMTP'06 here.
-
gabbay:genmn
-
Murdoch J. Gabbay
A General Mathematics of Names,
Information and Computation, Volume 205, Issue 7, July 2007, Pages 982-1011,
DOI 10.1016/j.ic.2006.10.010.
We present Fraenkel-Mostowski Generalised set theory. This generalises Fraenkel-Mostowski set theory (FM sets) to a theory which can interpret infinitary syntax (with infinitely many different names, which would violate the finite support property assumed in FM sets.
-
gabbay:frelog
-
Murdoch J. Gabbay,
Fresh Logic,
Journal of Applied Logic, Volume 5, Issue 2, June 2007, Pages 356-387, DOI 10.1016/j.jal.2005.10.012.
We give cut-free sequent and natural deduction logics which include a NEW-quantifier, freshness predicate, and swapping.
-
gabbay:nomu-jv
-
Christian Urban, Andrew M.Pitts and Murdoch J.Gabbay, Nominal
Unification, Theoretical Computer Science, Volume 323, Issues 1-3, 14 September 2004, Pages 473-497, DOI 10.1016/j.tcs.2004.06.016. (The conference paper is below.)
-
gabbay:picfm
-
Murdoch J. Gabbay,
The pi-calculus in FM,
In Thirty Five Years of Automating Mathematics, edited by
Fairouz Kamareddine,
Kluwer Applied Logic series. Volume 28. Pages 247-269.
November 2003.
ISBN 1-4020-1656-5.
-
gabbay:newaas-jv
-
Murdoch J. Gabbay and A.M. Pitts, A New Approach to Abstract
Syntax with Variable Binding, Formal Aspects of
Computing, special issue in honour of Rod Burstall, 2001.
(This is an extended and revised version of
gabbay:newaas.)
-
gabbay:lamcna
-
Murdoch J. Gabbay and Aad Mathijssen
The lambda-calculus is nominal algebraic,
in the Festschrift in Honour of Peter B. Andrews on his 70th Birthday.
We use nominal algebra to give a sound and complete axiomatisation of the lambda-calculus.
-
gabbay:alogic
-
Murdoch J. Gabbay and Michael Gabbay
a-logic,
in the Dov Gabbay 60th birthday festschrift.
We examine a simple but powerful extension of first-order logic with a predicate expressing the intensional properties of a term "this is a variable symbol". We apply it to axiomatise object-level explicit substition, object-level binding, and thus exhibit a finite first-order axiomatisation of the lambda-calculus.
-
gabbay:somfcg
-
Michael Gabbay and Murdoch J. Gabbay
Some Formal Considerations on Gabbay's Restart Rule in Natural Deduction and Goal-Directed Reasoning,
in the Dov Gabbay 60th birthday festschrift.
We investigate "Restart" a natural deduction rule which reads "from A we may deduce B". This powerful rule by Dov Gabbay in the 1980s adds many theorems to intuitionistic logic; we investigate them and consider generalisations. This paper is not a hoax.
-
gabbay:nomrs
-
Murdoch J. Gabbay and Martin Hofmann
Nominal renaming sets,
in LPAR'08.
We discuss nominal renaming sets.
These are like nominal sets, but based on a finitely-supported renaming action — a renaming is a function from atoms to atoms, not necessarily injective.
This provides a convenient sets-based semantics with which to justify Higher-Order Abstract Syntax.
-
gabbay:twoaah
-
Murdoch J. Gabbay and Dominic Mulligan
Two-and-a-halfth order lambda-calculus,
in WFLP'08.
We introduce two-and-a-halfth order lambda-calculus.
This introduces a functional operational semantics to the ‘unknowns’ of nominal terms; the result is a lambda-calculus in which both capturing and capture-avoiding substitution are represented, with a full (nominal terms style) theory of alpha-equivalence for level 1 variables (atoms) in the presence of level 2 variables (unknowns).
You might also like to look at the lambda-context calculus.
-
gabbay:tersl
-
Michael Gabbay and Murdoch J. Gabbay
Term sequent logic,
in WFLP'08.
We introduce term sequents which apply notions of intro-rule and sequent presentation for terms. We use this to build a logic for reasoning about the untyped lambda-calculus, similar to rewriting but with the power of first-order logic to deduce rewrites in the presence of assumptions.
-
gabbay:curhid
-
Murdoch J. Gabbay and Dominic Mulligan
One-and-a-halfth order terms: Curry-Howard for incomplete derivations,
in WOLLIC'08.
We apply nominal terms to propositions-as-types/proofs-as-terms in the presence of incomplete derivations.
Atoms correspond with assumptions, unknowns correspond with incomplete parts of the derivation, and a freshness condition corresponds with the condition that an assumption will be discharged in an unknown part of the derivation.
-
gabbay:subfmf
-
Murdoch J. Gabbay and Michael Gabbay
Substitution for Fraenkel-Mostowski Foundations,
in the AISB symposium on computing and philosophy.
We present a capture-avoiding substitution action on Fraenkel-Mostowski set theory.
Substitution is commonly understood as an action on syntax (for example when building a logic or a lambda calculus) and thus as a prelude to, but not a part of, mathematical denotations.
We show that it also has denotational reality as an operation on a mathematical foundation.
-
gabbay:lamcc
-
Murdoch J. Gabbay and Stéphane Lengrand
The lambda-context calculus,
in LFMTP'07, DOI j.entcs.2007.09.015; also online at ENTCS volume 196.
We present a simple lambda-calculus whose syntax is populated by variables which behave like meta-variables.
It can express both capture-avoiding and capturing substitution (instantiation).
-
gabbay:alwa
-
Murdoch J. Gabbay and Michael J. Gabbay
a-logic with arrows,
in WFLP'2007; see also the proceedings of the entire workshop and the full journal paper.
In a previous paper we discussed a-logic, a logic with a predicate ‘atom’ which is related to PROLOG's ‘isvar’.
It identifies a term as a variable symbol.
This provokes technical difficulties in the logic analogous to the difficulties giving a logical semantics to isvar.
In this paper we give a completely overhauled proof-system, and a new denotational semantics, which resolve these technical issues by a directed notion of equality similar to a rewrite relation. The result is a greatly improved ability to axiomatise logic and computation.
-
gabbay:forcie
-
Murdoch J. Gabbay and Aad Mathijssen
A Formal Calculus for Informal Equality with Binding,
in WOLLIC'2007.
DOI 10.1007/978-3-540-73445-1_12.
We describe Nominal Algebra, a logical calculus for reasoning which directly supports binding.
-
gabbay:nomsos-nwpt
-
MohammadReza Mousavi, Michel A. Reniers and Murdoch J. Gabbay
Nominal SOS,
in NWPT'06.
We describe Nominal Structured Operational Semantics, a framework for specifying operational semantics within which proofs of congruence are carried out ‘once and for all’.
-
gabbay:noma-nwpt
-
Murdoch J. Gabbay and Aad Mathijssen
Nominal Algebra,
in NWPT'06.
We describe Nominal Algebra, an algebraic system which can directly encode systems-with-binding without using functions.
Slides of the accompanying talk are here, and a paper is here.
-
gabbay:curstn
-
Maribel Fernandez and Murdoch J. Gabbay
Curry-style types for nominal terms,
In TYPES'06.
Nominal terms are a representation of syntax-with-binding in the presence of explicit meta-variables and alpha-renaming.
Making this consistent with a functional type system is non-trivial because the same meta-variable may appear in different contexts and under different binders, so when that meta-variable is instantiated the same variable name may be injected into different contexts of abstractions.
-
gabbay:oneaah
-
Murdoch J. Gabbay and Aad Mathijssen
One-and-a-halfth-order logic,
in PPDP 2006.
DOI 10.1145/1140335.1140359.
We present a logic similar to first-order logic, but with predicate unknowns in nominal style. This permits schematic reasoning in the presence of ‘unknown predicates’ which may also occur under binders. We give both algebraic and sequent characterisations of derivability, prove their equivalence, prove cut-elimination of the sequent system, and show correctness with respect to first-order logic.
-
gabbay:capasn
-
Murdoch J. Gabbay and Aad Mathijssen
Capture-avoiding Substitution as a Nominal Algebra,
in ICTAC 2006.
We give a detailed investigation of the fundamental operation which is capture-avoiding substitution, investigated from the point of view of Nominal Algebra.
-
gabbay:soshop
-
MohammadReza Mousavi, Murdoch J. Gabbay and Michel Reniers
SOS for higher-order processes,
in CONCUR'2005.
We propose promoted PANTH, a Structural Operational Semantics framework which extends Bernstein's propoted tyft/tyxt format, and for which a suitable notion of higher-order bisimulation is a congruence.
-
gabbay:newcc
-
Murdoch J. Gabbay
A NEW calculus of contexts,
in PPDP'2005,
DOI 10.1145/1069774.1069783.
We introduce a lambda-calculus in which context substitution (which does not avoid capture) has the same status as ordinary beta-reduction. We claim the calculus is expressive and can encode dynamic binding, objects, and interesting properties associated to partial evaluation. We prove meta-properties which include an applicative characterisation of contextual equivalence.
-
gabbay:nomrng
-
Maribel Fernandez, Murdoch J. Gabbay
Nominal Rewriting with Name Generation: abstraction vs. locality,
in PPDP'2005.
We generalise and extend previous work on rewriting-with-variable-binding with a construct for name generation, and study its properties.
-
gabbay:seqcnl
-
Murdoch J. Gabbay and James Cheney
A Sequent Calculus for Nominal Logic,
DOI 10.1109/LICS.2004.6.
In LICS'04.
We consider a sequent calculus for Nominal Logic, consider notions of Logic Programming for it, and give a translation of Miller and Tiu's FOLN.
-
gabbay:nomr
-
Maribel Fernandez, Murdoch J. Gabbay, Ian Mackie
Nominal Rewriting,
in PPDP'04.
We generalise first-order rewriting with terms involving binding operations, using a nominal approach in which bound entities are explicitly named.
-
gabbay:frepbm
-
M. R. Shinwell, A.M. Pitts and M.J.Gabbay, FreshML:
Programming with Binders Made Simple, In Eighth ACM
SIGPLAN International Conference on Functional Programming (ICFP
2003), Uppsala, Sweden, pages 263-274 (ACM Press, 2003).
-
gabbay:nomser
-
Murdoch J. Gabbay,
Nominal Sets, Equivariance Reasoning, and Variable Binding,
A brief prose account of my talk at MLG'02 in Kinosaki, Japan.
-
gabbay:nomu
-
Christian Urban, Andrew Pitts, Murdoch J. Gabbay,
Nominal Unification,
M.Baaz (Ed.), Computer Science Logic and 8th Kurt Godel
Colloquium (CSL'03 &
KGC), Vienna, Austria. Proccedings. Lecture Notes in
Computer Science, Volume 2803, pages 513-527
(Springer-Verlag, 2003).
(See here for
formal verification of the results in this paper, carried out by
Urban using Isabelle.)
-
gabbay:fmhhotn
-
Murdoch J. Gabbay,
FM-HOL, a higher-order theory of names,
In F. Kamareddine (Ed.) Workshop on Thirty Five years of Automath, Informal Proceedings, Heriot-Watt University, Edinburgh, Scotland, April 2002.
-
gabbay:autfms
-
Murdoch J. Gabbay,
Automating Fraenkel-Mostowski Syntax,
In TPHOLs 2002, 15th International Conference on Theorem Proving in Higher Order Logics, 20-23 of August, 2002.
-
gabbay:metpbn
-
A. M. Pitts and Murdoch J. Gabbay, A Metalanguage for
Programming with Bound Names Modulo Renaming. In
R. Backhouse and J. N. Oliveira (Eds),
Mathematics of
Programme Construction, 5th International Conference,
MPC2000, Ponte de Lima, Portugal, July 2000. Proceedings.
Lecture Notes in Computer Science, Volume 1837 (Springer-Verlag,
2000), pages 230-255.
-
gabbay:newaas
-
M.J. Gabbay and A.M. Pitts, A New Approach to Abstract
Syntax Involving Binders, In Proceedings 14th Annual
IEEE Symposium on Logic in Computer Science, Trento, Italy,
July 1999, (IEEE Computer Society Press, 1999) pp 214-224.
On Citeseer.
-
gabbay:nomrs-tr
-
Murdoch J. Gabbay
Nominal renaming sets (technical report),
Technical report HW-MACS-TR-0058.
We explore ‘nominal sets’ based on a renaming action (possibly non-injective functions on atoms) instead of the more usual permutation action.
We find that Gabbay-Pitts atoms-abstraction coincides with functional abstraction, making a nice connection between the two notions of ‘abstract a variable’.
-
gabbay:nomahs-tr
-
Murdoch J. Gabbay and Aad Mathijssen
Nominal Algebra and the HSP theorem (technical report),
Technical report HW-MACS-TR-0057.
We prove the HSP (Homomorphism, Subalgebra, Product) theorem for Nominal Algebra, also known as Birkhoff's theorem.
-
gabbay:capasn-tr
-
Murdoch J. Gabbay and Aad Mathijssen
Capture-avoiding Substitution as a Nominal Algebra (technical report).
Technical report HW-MACS-TR-0053 studies the decidability and theory of models of a ‘nominal’ axiomatisation of capture-avoiding substitution.
-
gabbay:noma-tr
-
Murdoch J. Gabbay and Aad Mathijssen
Nominal Algebra (technical report),
Technical report HW-MACS-TR-0045 which includes a detailed treatment of proofs in nominal algebra.
-
gabbay:arboms
-
Murdoch J. Gabbay and Michael Gabbay
Arbitrary Objects in Mathematics and Semantics,
in the Paris Arché workshop on abstract objects in semantics and the philosophy of mathematics.
A photo of Michael delivering the talk is online here.
-
gabbay:towptp
-
Michael Gabbay and Murdoch J. Gabbay
Towards a Proof-Theoretic Approach to Plurality,
in the Paris Arché workshop on abstract objects in semantics and the philosophy of mathematics.
-
gabbay:setfnt
-
Murdoch J. Gabbay
The sets foundations of nominal techniques.
A survey and update paper describing a view of the foundations of nominal techniques.
I welcome comments.
-
gabbay:nomaua
-
Murdoch J. Gabbay and Aad Mathijssen
Nominal algebra: a universal algebra with names and binding,
a journal version of our WOLLIC'07 paper.
We describe Nominal Algebra, a logical calculus for reasoning which directly supports binding.
I welcome comments.
-
gabbay:freg
-
Murdoch J. Gabbay,
Fresh Graphs,
We introduce a new notion of ‘Fresh Graph’, this is a graph with binding, to model behaviour with dynamic allocation. We will finish this Real Soon Now.
-
gabbay:thesis
-
Murdoch J. Gabbay, A Theory of Inductive Definitions with Alpha-Equivalence, PhD Thesis, Cambridge University, 2001. Supervised by Andrew Pitts.
