Showing 1–16 of 16 results for author: Gabbay, M J

Semitopology: distributed collaborative action via topology, algebra, and logic

Authors: Murdoch J. Gabbay, Giuliano Losa

Abstract: We introduce semitopologies, a generalisation of point-set topology that removes the restriction that intersections of open sets need necessarily be open. The intuition is that points are participants in some distributed system, and an open set is a collection of participants that can collaborate to update their local state by taking a distributed collaborative action; we call this an actionable… ▽ More We introduce semitopologies, a generalisation of point-set topology that removes the restriction that intersections of open sets need necessarily be open. The intuition is that points are participants in some distributed system, and an open set is a collection of participants that can collaborate to update their local state by taking a distributed collaborative action; we call this an actionable coalition. What constitutes an actionable coalition depends on what actions we want to model. Intuitive examples include 'a group of people that is collectively strong enough to lift a rock', where the state update is very simply 'holding rock low' to 'holding rock high' and this update is common to all participants in the actionable coalition. Or, consider 'two people wishing to barter a can of juice for a bar of chocolate', in which case the coalition is any such pair and the state updates differ between participants to flip them between 'has/has no juice' and 'has/has no chocolate'. A characteristic of these systems is that state updates are local to the coalition, voluntary, may vary between participants, and are not assumed subject to permission or synchronisation by a central authority. Peer-to-peer computer networks, including filesharing and blockchain systems, provide motivating examples from computing. This monograph presents a comprehensive view of semitopologies which includes point-set semitopology, algebra, and logic inspired by these considerations. This is interesting in and of itself and it provides a conceptual framework within which to understand a useful class of distributed systems. △ Less

Submitted 29 May, 2024; v1 submitted 16 January, 2024; originally announced February 2024.

Comments: This document is a preprint of a monograph, which integrates material from papers arXiv:2303.09287 (for point-set semitopologies) and arXiv:2310.00956 (for algebra). This update updates the license to CC-BY 4.0

MSC Class: 54J99; 54A05; 06D50; 06F30; 46H15; 54J05 ACM Class: F.3.2; F.3.3

Nominal semantics for predicate logic: algebras, substitution, quantifiers, and limits

Authors: Gilles Dowek, Murdoch J. Gabbay

Abstract: We define a model of predicate logic in which every term and predicate, open or closed, has an absolute denotation independently of a valuation of the variables. For each variable a, the domain of the model contains an element [[a]] which is the denotation of the term a (which is also a variable symbol). Similarly, the algebra interpreting predicates in the model directly interprets open predicate… ▽ More We define a model of predicate logic in which every term and predicate, open or closed, has an absolute denotation independently of a valuation of the variables. For each variable a, the domain of the model contains an element [[a]] which is the denotation of the term a (which is also a variable symbol). Similarly, the algebra interpreting predicates in the model directly interprets open predicates. Because of this models must also incorporate notions of substitution and quantification. These notions are axiomatic, and need not be applied only to sets of syntax. We prove soundness and show how every 'ordinary' model (i.e. model based on sets and valuations) can be translated to one of our nominal models, and thus also prove completeness. △ Less

Submitted 27 December, 2023; originally announced December 2023.

Journal ref: Proceedings of the 9th Italian Convention on Computational Logic (CILC 2012), pages 104-118, CEUR Workshop Proceedings Volume 857, ISSN 1613-0073 (urn:nbn:de:0074-857-8). https://nbn-resolving.org/urn:nbn:de:0074-857-8

Permissive-Nominal Logic (journal version)

Authors: Gilles Dowek, Murdoch J. Gabbay

Abstract: Permissive-Nominal Logic (PNL) is an extension of first-order predicate logic in which term-formers can bind names in their arguments. This allows for direct axiomatisations with binders, such as of the lambda-binder of the lambda-calculus or the forall-binder of first-order logic. It also allows us to finitely axiomatise arithmetic, and similarly to axiomatise 'nominal' datatypes-with-binding. Ju… ▽ More Permissive-Nominal Logic (PNL) is an extension of first-order predicate logic in which term-formers can bind names in their arguments. This allows for direct axiomatisations with binders, such as of the lambda-binder of the lambda-calculus or the forall-binder of first-order logic. It also allows us to finitely axiomatise arithmetic, and similarly to axiomatise 'nominal' datatypes-with-binding. Just like first- and higher-order logic, equality reasoning is not necessary to alpha-rename. This gives PNL much of the expressive power of higher-order logic, but models and derivations of PNL are first-order in character, and the logic seems to strike a good balance between expressivity and simplicity. △ Less

Submitted 27 December, 2023; originally announced December 2023.

ACM Class: F.4.1; I.2.3

Journal ref: ACM Transactions on Computational Logic, Volume 13, Number 3, Article 20, Publication date: August 2012

PNL to HOL: from the logic of nominal sets to the logic of higher-order functions

Authors: Gilles Dowek, Murdoch J. Gabbay

Abstract: Permissive-Nominal Logic (PNL) extends first-order predicate logic with term-formers that can bind names in their arguments. It takes a semantics in (permissive-)nominal sets. In PNL, the forall-quantifier or lambda-binder are just term-formers satisfying axioms, and their denotation is functions on nominal atoms-abstraction. Then we have higher-order logic (HOL) and its models in ordinary (i.e.… ▽ More Permissive-Nominal Logic (PNL) extends first-order predicate logic with term-formers that can bind names in their arguments. It takes a semantics in (permissive-)nominal sets. In PNL, the forall-quantifier or lambda-binder are just term-formers satisfying axioms, and their denotation is functions on nominal atoms-abstraction. Then we have higher-order logic (HOL) and its models in ordinary (i.e. Zermelo-Fraenkel) sets; the denotation of forall or lambda is functions on full or partial function spaces. This raises the following question: how are these two models of binding connected? What translation is possible between PNL and HOL, and between nominal sets and functions? We exhibit a translation of PNL into HOL, and from models of PNL to certain models of HOL. It is natural, but also partial: we translate a restricted subsystem of full PNL to HOL. The extra part which does not translate is the symmetry properties of nominal sets with respect to permutations. To use a little nominal jargon: we can translate names and binding, but not their nominal equivariance properties. This seems reasonable since HOL -- and ordinary sets -- are not equivariant. Thus viewed through this translation, PNL and HOL and their models do different things, but they enjoy non-trivial and rich subsystems which are isomorphic. △ Less

Submitted 25 December, 2023; originally announced December 2023.

Comments: arXiv admin note: substantial text overlap with arXiv:1111.4611

MSC Class: 03B70 (primary); 68Q55 (secondary) ACM Class: F.3.0; F.3.2

Journal ref: Theoretical Computer Science, Volume 451, 14 September 2012, Pages 38-69

Permissive nominal terms and their unification: an infinite, co-infinite approach to nominal techniques

Authors: Gilles Dowek, Murdoch J. Gabbay, Dominic Mulligan

Abstract: Nominal terms extend first-order terms with binding. They lack some properties of first- and higher-order terms: Terms must be reasoned about in a context of 'freshness assumptions'; it is not always possible to 'choose a fresh variable symbol' for a nominal term; it is not always possible to 'alpha-convert a bound variable symbol' or to 'quotient by alpha-equivalence'; the notion of unifier is no… ▽ More Nominal terms extend first-order terms with binding. They lack some properties of first- and higher-order terms: Terms must be reasoned about in a context of 'freshness assumptions'; it is not always possible to 'choose a fresh variable symbol' for a nominal term; it is not always possible to 'alpha-convert a bound variable symbol' or to 'quotient by alpha-equivalence'; the notion of unifier is not based just on substitution. Permissive nominal terms closely resemble nominal terms but they recover these properties, and in particular the 'always fresh' and 'always rename' properties. In the permissive world, freshness contexts are elided, equality is fixed, and the notion of unifier is based on substitution alone rather than on nominal terms' notion of unification based on substitution plus extra freshness conditions. We prove that expressivity is not lost moving to the permissive case and provide an injection of nominal terms unification problems and their solutions into permissive nominal terms problems and their solutions. We investigate the relation between permissive nominal unification and higher-order pattern unification. We show how to translate permissive nominal unification problems and solutions in a sound, complete, and optimal manner, in suitable senses which we make formal. △ Less

Submitted 25 December, 2023; originally announced December 2023.

Journal ref: Logic Journal of the IGPL, Volume 18, Issue 6, December 2010, Pages 769-822

Algebras of UTxO blockchains

Authors: Murdoch J. Gabbay

Abstract: We condense the theory of blockchains down to a simple and compact set of four type equations (Idealised EUTxO), and to an algebraic characterisation (abstract chunk systems), and exhibit an adjoint pair of functors between them. This gives a novel account of the essential mathematical structures underlying blockchain technology, such as Bitcoin. We condense the theory of blockchains down to a simple and compact set of four type equations (Idealised EUTxO), and to an algebraic characterisation (abstract chunk systems), and exhibit an adjoint pair of functors between them. This gives a novel account of the essential mathematical structures underlying blockchain technology, such as Bitcoin. △ Less

Submitted 6 September, 2021; v1 submitted 24 July, 2020; originally announced July 2020.

MSC Class: 03B70; 68Q55; 68Q65 ACM Class: D.3.1; F.3.2

UTxO- vs account-based smart contract blockchain programming paradigms

Authors: Lars Brunjes, Murdoch J. Gabbay

Abstract: We implement two versions of a simple but illustrative smart contract: one in Solidity on the Ethereum blockchain platform, and one in Plutus on the Cardano platform, with annotated code excerpts and with source code attached. We get a clearer view of the Cardano programming model in particular by introducing a novel mathematical abstraction which we call Idealised EUTxO. For each version of the c… ▽ More We implement two versions of a simple but illustrative smart contract: one in Solidity on the Ethereum blockchain platform, and one in Plutus on the Cardano platform, with annotated code excerpts and with source code attached. We get a clearer view of the Cardano programming model in particular by introducing a novel mathematical abstraction which we call Idealised EUTxO. For each version of the contract, we trace how the architectures of the underlying platforms and their mathematics affects the natural programming styles and natural classes of errors. We prove some simple but novel results about alpha-conversion and observational equivalence for Cardano, and explain why Ethereum does not have them. We conclude with a wide-ranging and detailed discussion in the light of the examples, mathematical model, and mathematical results so far. △ Less

Submitted 20 July, 2020; v1 submitted 31 March, 2020; originally announced March 2020.

MSC Class: 03B70; 68Q60 ACM Class: D.3.1; F.3.1

Equivariant ZFA with Choice: a position paper

Authors: Murdoch J. Gabbay

Abstract: We propose Equivariant ZFA with Choice as a foundation for nominal techniques that is stronger than ZFC and weaker than FM, and why this may be particularly helpful in the context of automated reasoning. We propose Equivariant ZFA with Choice as a foundation for nominal techniques that is stronger than ZFC and weaker than FM, and why this may be particularly helpful in the context of automated reasoning. △ Less

Submitted 23 March, 2018; originally announced March 2018.

Comments: In ARW 2018

ACM Class: F.4.1; F.3.1; D.2.4; D.3.1

Equivariant ZFA and the foundations of nominal techniques

Authors: Murdoch J. Gabbay

Abstract: We give an accessible presentation to the foundations of nominal techniques, lying between Zermelo-Fraenkel set theory and Fraenkel-Mostowski set theory, and which has several nice properties including being consistent with the Axiom of Choice. We give two presentations of equivariance, accompanied by detailed yet user-friendly discussions of its theoretical significance and practical application. We give an accessible presentation to the foundations of nominal techniques, lying between Zermelo-Fraenkel set theory and Fraenkel-Mostowski set theory, and which has several nice properties including being consistent with the Axiom of Choice. We give two presentations of equivariance, accompanied by detailed yet user-friendly discussions of its theoretical significance and practical application. △ Less

Submitted 22 January, 2020; v1 submitted 29 January, 2018; originally announced January 2018.

ACM Class: F.4.1; F.3.1; D.2.4; D.3.1

The language of Stratified Sets is confluent and strongly normalising

Authors: Murdoch J. Gabbay

Abstract: We study the properties of the language of Stratified Sets (first-order logic with $\in$ and a stratification condition) as used in TST, TZT, and (with stratifiability instead of stratification) in Quine's NF. We find that the syntax forms a nominal algebra for substitution and that stratification and stratifiability imply confluence and strong normalisation under rewrites corresponding naturally… ▽ More We study the properties of the language of Stratified Sets (first-order logic with $\in$ and a stratification condition) as used in TST, TZT, and (with stratifiability instead of stratification) in Quine's NF. We find that the syntax forms a nominal algebra for substitution and that stratification and stratifiability imply confluence and strong normalisation under rewrites corresponding naturally to $β$-conversion. △ Less

Submitted 20 May, 2018; v1 submitted 22 May, 2017; originally announced May 2017.

Comments: arXiv admin note: text overlap with arXiv:1406.4060

ACM Class: D.3.1; F.3.2; F.4.1

Journal ref: Logical Methods in Computer Science, Volume 14, Issue 2 (May 23, 2018) lmcs:3681

Consistency of Quine's New Foundations

Authors: Murdoch J. Gabbay

Abstract: We provide an elementary consistency proof of Quine's New Foundations, by a construction using interated nominal powersets. We provide an elementary consistency proof of Quine's New Foundations, by a construction using interated nominal powersets. △ Less

Submitted 30 June, 2023; v1 submitted 16 June, 2014; originally announced June 2014.

Comments: Corrected a few typos and added remark on consistency strength

MSC Class: 03E35 (Primary); 03B70 (Secondary) ACM Class: F.4.1

Semantics out of context: nominal absolute denotations for first-order logic and computation

Authors: Murdoch J. Gabbay

Abstract: Call a semantics for a language with variables absolute when variables map to fixed entities in the denotation. That is, a semantics is absolute when the denotation of a variable a is a copy of itself in the denotation. We give a trio of lattice-based, sets-based, and algebraic absolute semantics to first-order logic. Possibly open predicates are directly interpreted as lattice elements / sets / a… ▽ More Call a semantics for a language with variables absolute when variables map to fixed entities in the denotation. That is, a semantics is absolute when the denotation of a variable a is a copy of itself in the denotation. We give a trio of lattice-based, sets-based, and algebraic absolute semantics to first-order logic. Possibly open predicates are directly interpreted as lattice elements / sets / algebra elements, subject to suitable interpretations of the connectives and quantifiers. In particular, universal quantification "forall a.phi" is interpreted using a new notion of "fresh-finite" limit and using a novel dual to substitution. The interest of this semantics is partly in the non-trivial and beautiful technical details, which also offer certain advantages over existing semantics---but also the fact that such semantics exist at all suggests a new way of looking at variables and the foundations of logic and computation, which may be well-suited to the demands of modern computer science. △ Less

Submitted 5 January, 2016; v1 submitted 27 May, 2013; originally announced May 2013.

ACM Class: F.4.1; F.3.2

Representation and duality of the untyped lambda-calculus in nominal lattice and topological semantics, with a proof of topological completeness

Authors: Murdoch J. Gabbay, Michael J. Gabbay

Abstract: We give a semantics for the lambda-calculus based on a topological duality theorem in nominal sets. A novel interpretation of lambda is given in terms of adjoints, and lambda-terms are interpreted absolutely as sets (no valuation is necessary). We give a semantics for the lambda-calculus based on a topological duality theorem in nominal sets. A novel interpretation of lambda is given in terms of adjoints, and lambda-terms are interpreted absolutely as sets (no valuation is necessary). △ Less

Submitted 6 October, 2016; v1 submitted 25 May, 2013; originally announced May 2013.

ACM Class: F.4.1; F.3.2

Finite and infinite support in nominal algebra and logic: nominal completeness theorems for free

Authors: Murdoch J. Gabbay

Abstract: By operations on models we show how to relate completeness with respect to permissive-nominal models to completeness with respect to nominal models with finite support. Models with finite support are a special case of permissive-nominal models, so the construction hinges on generating from an instance of the latter, some instance of the former in which sufficiently many inequalities are preserved… ▽ More By operations on models we show how to relate completeness with respect to permissive-nominal models to completeness with respect to nominal models with finite support. Models with finite support are a special case of permissive-nominal models, so the construction hinges on generating from an instance of the latter, some instance of the former in which sufficiently many inequalities are preserved between elements. We do this using an infinite generalisation of nominal atoms-abstraction. The results are of interest in their own right, but also, we factor the mathematics so as to maximise the chances that it could be used off-the-shelf for other nominal reasoning systems too. Models with infinite support can be easier to work with, so it is useful to have a semi-automatic theorem to transfer results from classes of infinitely-supported nominal models to the more restricted class of models with finite support. In conclusion, we consider different permissive-nominal syntaxes and nominal models and discuss how they relate to the results proved here. △ Less

Submitted 5 December, 2011; originally announced December 2011.

MSC Class: 03B70 (Primary) 68Q55 (Secondary) ACM Class: F.3.0; F.3.2

Nominal Henkin Semantics: simply-typed lambda-calculus models in nominal sets

Authors: Murdoch J. Gabbay, Dominic P. Mulligan

Abstract: We investigate a class of nominal algebraic Henkin-style models for the simply typed lambda-calculus in which variables map to names in the denotation and lambda-abstraction maps to a (non-functional) name-abstraction operation. The resulting denotations are smaller and better-behaved, in ways we make precise, than functional valuation-based models. Using these new models, we then develop a g… ▽ More We investigate a class of nominal algebraic Henkin-style models for the simply typed lambda-calculus in which variables map to names in the denotation and lambda-abstraction maps to a (non-functional) name-abstraction operation. The resulting denotations are smaller and better-behaved, in ways we make precise, than functional valuation-based models. Using these new models, we then develop a generalisation of λ-term syntax enriching them with existential meta-variables, thus yielding a theory of incomplete functions. This incompleteness is orthogonal to the usual notion of incompleteness given by function abstraction and application, and corresponds to holes and incomplete objects. △ Less

Submitted 31 October, 2011; originally announced November 2011.

Comments: In Proceedings LFMTP 2011, arXiv:1110.6685

ACM Class: F.4.1(mathematical logic); F.3.2(algebraic approaches to semantics); D.3.1(semantics)

Journal ref: EPTCS 71, 2011, pp. 58-75

Closed nominal rewriting and efficiently computable nominal algebra equality

Authors: Maribel Fernández, Murdoch J. Gabbay

Abstract: We analyse the relationship between nominal algebra and nominal rewriting, giving a new and concise presentation of equational deduction in nominal theories. With some new results, we characterise a subclass of equational theories for which nominal rewriting provides a complete procedure to check nominal algebra equality. This subclass includes specifications of the lambda-calculus and first-o… ▽ More We analyse the relationship between nominal algebra and nominal rewriting, giving a new and concise presentation of equational deduction in nominal theories. With some new results, we characterise a subclass of equational theories for which nominal rewriting provides a complete procedure to check nominal algebra equality. This subclass includes specifications of the lambda-calculus and first-order logic. △ Less

Submitted 14 September, 2010; originally announced September 2010.

Comments: In Proceedings LFMTP 2010, arXiv:1009.2189

Journal ref: EPTCS 34, 2010, pp. 37-51