Separation and Renaming in Nominal Sets

Joshua Moerman; Jurriaan Rot

doi:10.4230/LIPIcs.CSL.2020.31

Separation and Renaming in Nominal Sets

Research output: Chapter in Book/Report/Conference proceeding › Conference Article in proceeding › Academic › peer-review

Abstract

Nominal sets provide a foundation for reasoning about names. They are used primarily in syntax with binders, but also, e.g., to model automata over infinite alphabets. In this paper, nominal sets are related to nominal renaming sets, which involve arbitrary substitutions rather than permutations, through a categorical adjunction. In particular, the left adjoint relates the separated product of nominal sets to the Cartesian product of nominal renaming sets. Based on these results, we define the new notion of separated nominal automata. We show that these automata can be exponentially smaller than classical nominal automata, if the semantics is closed under substitutions.

Original language	English
Title of host publication	CSL
Subtitle of host publication	28th EACSL Annual Conference on Computer Science Logic
Editors	Maribel Fernandez, Anca Muscholl
Publisher	Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
Pages	31:1-31:17
Number of pages	17
ISBN (Print)	978-3-95977-132-0
DOIs	https://doi.org/10.4230/LIPIcs.CSL.2020.31
Publication status	Published - Jan 2020
Externally published	Yes
Event	28th EACSL Annual Conference on Computer Science Logic - Barcelona, Spain Duration: 13 Jan 2020 → 16 Jan 2020 Conference number: 28 https://drops.dagstuhl.de/opus/volltexte/2020/11643/pdf/LIPIcs-CSL-2020-0.pdf

Conference

Conference	28th EACSL Annual Conference on Computer Science Logic
Abbreviated title	CSL 2020
Country/Territory	Spain
City	Barcelona
Period	13/01/20 → 16/01/20
Internet address	https://drops.dagstuhl.de/opus/volltexte/2020/11643/pdf/LIPIcs-CSL-2020-0.pdf

Keywords

Adjunction
Automata
Coalgebra
Nominal sets
Separated product

Access to Document

10.4230/LIPIcs.CSL.2020.31Licence: CC BY

Cite this

@inproceedings{f2fb322c417844618e192cfb95ecdb08,

title = "Separation and Renaming in Nominal Sets",

abstract = "Nominal sets provide a foundation for reasoning about names. They are used primarily in syntax with binders, but also, e.g., to model automata over infinite alphabets. In this paper, nominal sets are related to nominal renaming sets, which involve arbitrary substitutions rather than permutations, through a categorical adjunction. In particular, the left adjoint relates the separated product of nominal sets to the Cartesian product of nominal renaming sets. Based on these results, we define the new notion of separated nominal automata. We show that these automata can be exponentially smaller than classical nominal automata, if the semantics is closed under substitutions.",

keywords = "Adjunction, Automata, Coalgebra, Nominal sets, Separated product",

author = "Joshua Moerman and Jurriaan Rot",

note = "DBLP License: DBLP's bibliographic metadata records provided through http://dblp.org/ are distributed under a Creative Commons CC0 1.0 Universal Public Domain Dedication. Although the bibliographic metadata records are provided consistent with CC0 1.0 Dedication, the content described by the metadata records is not. Content may be subject to copyright, rights of privacy, rights of publicity and other restrictions.; 28th EACSL Annual Conference on Computer Science Logic, CSL 2020 ; Conference date: 13-01-2020 Through 16-01-2020",

year = "2020",

month = jan,

doi = "10.4230/LIPIcs.CSL.2020.31",

language = "English",

isbn = "978-3-95977-132-0",

pages = "31:1--31:17",

editor = "Maribel Fernandez and Anca Muscholl",

booktitle = "CSL",

publisher = "Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing",

address = "Germany",

url = "https://drops.dagstuhl.de/opus/volltexte/2020/11643/pdf/LIPIcs-CSL-2020-0.pdf",

}

Moerman, J & Rot, J 2020, Separation and Renaming in Nominal Sets. in M Fernandez & A Muscholl (eds), CSL: 28th EACSL Annual Conference on Computer Science Logic., 31, Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, pp. 31:1-31:17, 28th EACSL Annual Conference on Computer Science Logic, Barcelona, Spain, 13/01/20. https://doi.org/10.4230/LIPIcs.CSL.2020.31

Separation and Renaming in Nominal Sets. / Moerman, Joshua; Rot, Jurriaan.
CSL: 28th EACSL Annual Conference on Computer Science Logic. ed. / Maribel Fernandez; Anca Muscholl. Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, 2020. p. 31:1-31:17 31.

Research output: Chapter in Book/Report/Conference proceeding › Conference Article in proceeding › Academic › peer-review

TY - GEN

T1 - Separation and Renaming in Nominal Sets

AU - Moerman, Joshua

AU - Rot, Jurriaan

N1 - Conference code: 28

PY - 2020/1

Y1 - 2020/1

N2 - Nominal sets provide a foundation for reasoning about names. They are used primarily in syntax with binders, but also, e.g., to model automata over infinite alphabets. In this paper, nominal sets are related to nominal renaming sets, which involve arbitrary substitutions rather than permutations, through a categorical adjunction. In particular, the left adjoint relates the separated product of nominal sets to the Cartesian product of nominal renaming sets. Based on these results, we define the new notion of separated nominal automata. We show that these automata can be exponentially smaller than classical nominal automata, if the semantics is closed under substitutions.

AB - Nominal sets provide a foundation for reasoning about names. They are used primarily in syntax with binders, but also, e.g., to model automata over infinite alphabets. In this paper, nominal sets are related to nominal renaming sets, which involve arbitrary substitutions rather than permutations, through a categorical adjunction. In particular, the left adjoint relates the separated product of nominal sets to the Cartesian product of nominal renaming sets. Based on these results, we define the new notion of separated nominal automata. We show that these automata can be exponentially smaller than classical nominal automata, if the semantics is closed under substitutions.

KW - Adjunction

KW - Automata

KW - Coalgebra

KW - Nominal sets

KW - Separated product

U2 - 10.4230/LIPIcs.CSL.2020.31

DO - 10.4230/LIPIcs.CSL.2020.31

M3 - Conference Article in proceeding

SN - 978-3-95977-132-0

SP - 31:1-31:17

BT - CSL

A2 - Fernandez, Maribel

A2 - Muscholl, Anca

PB - Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing

T2 - 28th EACSL Annual Conference on Computer Science Logic

Y2 - 13 January 2020 through 16 January 2020

ER -

Separation and Renaming in Nominal Sets

Abstract

Conference

Keywords

Access to Document

Fingerprint

Cite this