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

DOI10.1016/J.TCS.2012.06.007zbMATH Open1309.03013arXiv1111.4611OpenAlexW2163198641MaRDI QIDQ714797FDOQ714797

Authors: Gilles Dowek, Murdoch J. Gabbay 

Publication date: 11 October 2012

Published in: Theoretical Computer Science (Search for Journal in Brave)

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. 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.

Full work available at URL: https://arxiv.org/abs/1111.4611

Recommendations

• Permissive-nominal logic: first-order logic over nominal terms and sets
• scientific article; zbMATH DE number 2242589
• Nominal logic, a first order theory of names and binding
• A simple nominal type theory
• Fresh logic: Proof-theory and semantics for FM and nominal techniques

zbMATH Keywords

higher-order logicnominal setsmathematical foundations of programmingnominal renaming setspermissive-nominal logic

Mathematics Subject Classification ID

Logic in computer science (03B70) Functional programming and lambda calculus (68N18)

Cites Work

• Title not available (Why is that?)
• Untersuchungen über das logische Schliessen. I
• Nominal logic, a first order theory of names and binding
• Foundations of nominal techniques: logic and semantics of variables in abstract syntax
• A Nominal Axiomatization of the Lambda Calculus
• Nominal (universal) algebra: equational logic with names and binding
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• A new approach to abstract syntax with variable binding
• Nominal unification
• Title not available (Why is that?)
• Title not available (Why is that?)
• A formulation of the simple theory of types
• Programming with higher-order logic.
• Higher-order semantics and extensionality
• Title not available (Why is that?)
• Towards nominal computation
• About permutation algebras, (pre)sheaves and named sets
• Unification under a mixed prefix
• Theorem proving modulo
• Higher-order rewrite systems and their confluence
• A study of substitution, using nominal techniques and Fraenkel-Mostowksi sets
• Finite and infinite support in nominal algebra and logic: nominal completeness theorems for free
• Permissive-nominal logic
• Permissive nominal terms and their unification: an infinite, co-infinite approach to nominal techniques
• Two-level nominal sets and semantic nominal terms: an extension of nominal set theory for handling meta-variables
• One-and-a-halfth-order Logic
• Capture-Avoiding Substitution as a Nominal Algebra
• A Formal Calculus for Informal Equality with Binding
• Nominal Renaming Sets
• Nominal Unification from a Higher-Order Perspective
• A general mathematics of names
• Capture-avoiding substitution as a nominal algebra
• Primitive recursion for higher-order abstract syntax
• Logic Programming
• Explicit substitutions
• Fresh logic: Proof-theory and semantics for FM and nominal techniques
• A proof theory for generic judgments
• Completeness and Herbrand theorems for nominal logic
• The seven virtues of simple type theory
• The lambda-context calculus (extended version)
• The \(\lambda\)-context calculus
• Second-Order Equational Logic (Extended Abstract)
• A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification
• Meta-variables as infinite lists in nominal terms unification and rewriting

Cited In (1)

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

Uses Software

• ETPS

This page was built for publication: PNL to HOL: from the logic of nominal sets to the logic of higher-order functions

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q714797)