DROPS

Document

DOI: 10.4230/LIPIcs.CSL.2025.44

Classical Linear Logic in Perfect Banach Lattices

Authors: Pedro H. Azevedo de Amorim, Leon Witzman, and Dexter Kozen

Published in: LIPIcs, Volume 326, 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)

Abstract

In recent years, researchers have proposed various models of linear logic with strong connections to measure theory, with probabilistic coherence spaces (PCoh) being one of the most prominent. One of the main limitations of the PCoh model is that it cannot interpret continuous measures. To overcome this obstacle, Ehrhard has extended PCoh to a category of positive cones and linear Scott-continuous functions and shown that it is a model of intuitionistic linear logic. In this work we show that the category PBanLat₁ of perfect Banach lattices and positive linear functions of norm at most 1 can serve the same purpose, with some added benefits. We show that PBanLat₁ is a model of classical linear logic (without exponential) and that PCoh embeds fully and faithfully in PBanLat₁ while preserving the monoidal and *-autonomous structures. Finally, we show how PBanLat₁ can be used to give semantics to a higher-order probabilistic programming language.

Cite as

Pedro H. Azevedo de Amorim, Leon Witzman, and Dexter Kozen. Classical Linear Logic in Perfect Banach Lattices. In 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 326, pp. 44:1-44:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{azevedodeamorim_et_al:LIPIcs.CSL.2025.44,
  author =	{Azevedo de Amorim, Pedro H. and Witzman, Leon and Kozen, Dexter},
  title =	{{Classical Linear Logic in Perfect Banach Lattices}},
  booktitle =	{33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)},
  pages =	{44:1--44:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-362-1},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{326},
  editor =	{Endrullis, J\"{o}rg and Schmitz, Sylvain},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2025.44},
  URN =		{urn:nbn:de:0030-drops-228013},
  doi =		{10.4230/LIPIcs.CSL.2025.44},
  annote =	{Keywords: Probabilistic Semantics, Linear Logic, Categorical Semantics}
}

Document

DOI: 10.4230/LIPIcs.FUN.2021.10

Computational Fun with Sturdy and Flimsy Numbers

Authors: Trevor Clokie, Thomas F. Lidbetter, Antonio J. Molina Lovett, Jeffrey Shallit, and Leon Witzman

Published in: LIPIcs, Volume 157, 10th International Conference on Fun with Algorithms (FUN 2021) (2020)

Abstract

Following Stolarsky, we say that a natural number n is flimsy in base b if some positive multiple of n has smaller digit sum in base b than n does; otherwise it is sturdy . We develop algorithmic methods for the study of sturdy and flimsy numbers. We provide some criteria for determining whether a number is sturdy. Focusing on the case of base b = 2, we study the computational problem of checking whether a given number is sturdy, giving several algorithms for the problem. We find two additional, previously unknown sturdy primes. We develop a method for determining which numbers with a fixed number of 0’s in binary are flimsy. Finally, we develop a method that allows us to estimate the number of k-flimsy numbers with n bits, and we provide explicit results for k = 3 and k = 5. Our results demonstrate the utility (and fun) of creating algorithms for number theory problems, based on methods of automata theory.

Cite as

Trevor Clokie, Thomas F. Lidbetter, Antonio J. Molina Lovett, Jeffrey Shallit, and Leon Witzman. Computational Fun with Sturdy and Flimsy Numbers. In 10th International Conference on Fun with Algorithms (FUN 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 157, pp. 10:1-10:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{clokie_et_al:LIPIcs.FUN.2021.10,
  author =	{Clokie, Trevor and Lidbetter, Thomas F. and Molina Lovett, Antonio J. and Shallit, Jeffrey and Witzman, Leon},
  title =	{{Computational Fun with Sturdy and Flimsy Numbers}},
  booktitle =	{10th International Conference on Fun with Algorithms (FUN 2021)},
  pages =	{10:1--10:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-145-0},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{157},
  editor =	{Farach-Colton, Martin and Prencipe, Giuseppe and Uehara, Ryuhei},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FUN.2021.10},
  URN =		{urn:nbn:de:0030-drops-127715},
  doi =		{10.4230/LIPIcs.FUN.2021.10},
  annote =	{Keywords: sturdy number, flimsy number, context-free grammar, finite automaton, enumeration}
}

Search Results

Documents authored by Witzman, Leon

Classical Linear Logic in Perfect Banach Lattices

Abstract

Cite as

Computational Fun with Sturdy and Flimsy Numbers

Abstract

Cite as

Thanks for your feedback!

Could not send message