Geometry of Resource Interaction - A Minimalist Approach

Marco Solieri

doi:10.4204/eptcs.176.7

Home/Archive/arXiv

arXiv · 1502.04775

Geometry of Resource Interaction - A Minimalist Approach

Marco Solieri

View original source ↗Read source document ↗Export metadata ↓

Abstract

The Resource $λ$-calculus is a variation of the $λ$-calculus where arguments can be superposed and must be linearly used. Hence it is a model for linear and non-deterministic programming languages, and the target language of Ehrhard-Taylor expansion of $λ$-terms. In a strictly typed restriction of the Resource $λ$-calculus, we study the notion of path persistence, and we define a Geometry of Interaction that characterises it, is invariant under reduction, and counts addends in normal forms.

Explore related subjects

cs.LO cs.PL

Keep this discovery

Explore connections, maps & timelines

BibTeX RIS

Marco Solieri. 2015-02-17. Geometry of Resource Interaction - A Minimalist Approach. https://doi.org/10.4204/eptcs.176.7

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

KEEP EXPLORING

Related papers

arXiv2026

JustAct: A Framework for Auditable Multi-Agent Systems Regulated by Inter-Organisational Policies

In open multi-agent agent systems that cross organisational boundaries, agent actions must be regulated by complex policies. Consider medical data processing systems, which must observe generic laws (e.g., EU data protection regulations) and also specific participants' resource conditions (e.g., Bob consents to sharing his X-Rays with EU hospitals). Presently, we address the implementation of these systems as distributed software. Solutions to key sub-problems are available: existing policy languages capture the necessary normative concepts and formalise the computational representation and reasoning about policies, and existing distributed algorithms and protocols coordinate agents' changing actions and policies. But which policies and protocols are useful in application? With the JustAct framework, we characterise a class of multi-agent systems where actors justify their actions with sufficient policy information collected from dynamic policy statements and agreements. We prove key properties of these systems, e.g., any decision that an action is permitted now cannot be refuted later, regardless of any added statements or updated agreements. We study a particular instance of the framework by specifying (in Rocq) and implementing (in Rust) a particular policy language and runtime system for mediating agent communications. We demonstrate and assess JustAct via a case study of this implementation: we reproduce the usage scenarios of Brane, an existing policy-regulated, inter-domain, medical data processing system.

cs.LO↗

arXiv2026

Undefinability of Approximation of 2-to-2 Games

Recent work by Atserias and Dawar (J. Log. Comp 2019) and Tucker-Foltz (LMCS 2024) has established undefinability results in fixed-point logic with counting (FPC) corresponding to many classical complexity results from the hardness of approximation. In this line of work, NP-hardness results are turned into unconditional FPC undefinability results. We extend this work by showing the FPC undefinability of any constant factor approximation of weighted 2-to-2 games, based on the NP-hardness results of Khot, Minzer and Safra. Our result shows that the completely satisfiable 2-to-2 games are not FPC-separable from those that are not epsilon-satisfiable, for arbitrarily small epsilon. The perfect completeness of our inseparability is an improvement on the complexity result, as the NP-hardness of such a separation is still only conjectured. This perfect completeness enables us to show the FPC undefinability of other problems whose NP-hardness is conjectured. In particular, we are able to show that no FPC formula can separate the 3-colourable graphs from those that are not t-colourable, for any constant t.

cs.LO↗

arXiv2026

Possibilistic Computation Tree Logic over Finitely-Valued Kripke Structures: Decidability and Complete Axiomatization

Possibilistic computation tree logic (PoCTL) is a branching-time temporal logic for specifying and verifying systems whose behavior is described by possibility theory. Although the model-checking problem for PoCTL has been investigated, its satisfiability problem and proof-theoretic foundations, particularly the development of a sound and complete axiomatization,remain largely unexplored. We investigate these problems over normalized possibilistic Kripke structures whose transition possibilities take finitely many values; their state spaces may be countably infinite. A counterexample shows that unrestricted countable structures do not have the finite-model property, thereby distinguishing the semantic scope of the present results. For the finitely-valued class, we extract a finite threshold scale from the input formula and define canonical admissible transitions by the set $D(s,t)$. Independent eventuality ranks guide the selection of local witnesses. Finite supported fragments are then spliced cyclically to obtain a model, without requiring the ranks of different eventualities to decrease simultaneously. This yields a finite-model property. Satisfiability for the unbounded language over this class is EXPTIME-complete, and the tableau procedure runs in time $2^{O(n^2)}$. Bounded operators are handled by explicit finite unfolding, with complexity measured after this preprocessing. Finally, we establish a sound and weakly complete finitary axiomatization by translating tableau deletion into formal refutations.

cs.LO↗