Search arXiv⌕ Search
Home/Archive/arXiv

arXiv · cs/0410030

Weak Typed Boehm Theorem on IMLL

Satoshi Matsuoka
View original source ↗Read source document ↗Export metadata ↓

Abstract

In the Boehm theorem workshop on Crete island, Zoran Petric called Statman's ``Typical Ambiguity theorem'' typed Boehm theorem. Moreover, he gave a new proof of the theorem based on set-theoretical models of the simply typed lambda calculus. In this paper, we study the linear version of the typed Boehm theorem on a fragment of Intuitionistic Linear Logic. We show that in the multiplicative fragment of intuitionistic linear logic without the multiplicative unit 1 (for short IMLL) weak typed Boehm theorem holds. The system IMLL exactly corresponds to the linear lambda calculus without exponentials, additives and logical constants. The system IMLL also exactly corresponds to the free symmetric monoidal closed category without the unit object. As far as we know, our separation result is the first one with regard to these systems in a purely syntactical manner.

Explore related subjects

cs.LO

Keep this discovery

Explore connections, maps & timelines

BibTeXRIS

Satoshi Matsuoka. 2005-04-16. Weak Typed Boehm Theorem on IMLL. https://doi.org/10.1016/j.apal.2006.06.001

Cite the original work for its findings. Save a collection to share your selection of sources.

KEEP EXPLORING

Related papers

arXiv2026

The Yoneda embedding in simplicial type theory

Riehl and Shulman introduced simplicial type theory (STT), a variant of homotopy type theory which aimed to study not just homotopy theory, but its fusion with category theory: $(\infty,1)$-category theory. While notoriously technical, manipulating $\infty$-categories in simplicial type theory is often easier than working with ordinary categories, with the type theory handling infinite stacks of coherences in the background. We capitalize on recent work by Gratzer et al. defining the $(\infty,1)$-category of $\infty$-groupoids in STT to define presheaf categories within STT and systematically develop their theory. In particular, we construct the Yoneda embedding, prove the universal property of presheaf categories, refine the theory of adjunctions in STT, introduce the theory of Kan extensions, and prove Quillen's Theorem A.

cs.LO↗
arXiv2026

The Program Logic of Abstract Interpretation

Hoare-style program logics and abstract interpretation are two of the principal frameworks for reasoning about programs, and their affinity has long been recognised informally: both derive over-approximate judgements about program behaviour by structural, syntax-directed reasoning. Turning this analogy into a formal correspondence runs into two challenges. First, the disjunction (or join) rule, sound and admissible in Hoare logic, becomes unsound over non-additive abstract semantics. Second, the extrapolation operators that make abstract interpretation effective on unbounded computations, i.e. widening and narrowing, have no analogue in the derivations of existing program logics. We introduce APPL (Abstract Program Property Logic), a Hoare-style program logic that provides a proof-theoretic foundation for abstract interpretation while addressing both challenges. The key technical idea is density: abstract semantics is additive over dense families of logical assertions. This leads to a density-guarded join rule that enables sound disjunctive reasoning over arbitrary abstract domains. We also internalise the application of widening and narrowing through inference rules for iterative commands. As a result, an entire analysis by abstract interpretation can be viewed as a logical derivation in APPL. The logic is sound over any abstract domain and, when the assertion language is expressive enough, it is also relatively complete. Finally, by interpreting nondeterminism through a monoidal operator, APPL provides a single logical framework that uniformly subsumes Hoare logic, incorrectness logic, and Hoare-style logics for hyperproperties, thereby enabling their abstraction. Remarkably, the density-guarded join rule introduced to handle non-additive abstract semantics is also fundamental in guaranteeing completeness for hyperproperties.

cs.LO↗
arXiv2026

Optimal Probabilistic Answer Set Programming: Complexity and Implementations

Probabilistic Answer Set Programming (PASP) extends Answer Set Programming with the possibility of representing uncertain data. Among the possible available semantics, we focus here on the credal semantics. In this setting, prior work has focused exclusively on plain ASP programs, i.e., programs without optimization constructs. However, many real world tasks define optimality criteria over the possible solutions, which cannot be conveniently modeled with existing probabilistic ASP frameworks. In this paper, we close this gap and propose optimal Probabilistic Answer Set Programming, which extends PASP by also allowing weak constraints, which are the standard optimization construct of ASP. We define the semantics of such programs, study the computational complexity of the inference and most probable explanation tasks, and propose practical implementations based on Algebraic Model Counting and Answer Set Programming with Quantifiers. An empirical evaluation of the proposed approach on three real world tasks confirms the applicability of our framework.

cs.LO↗