583 research outputs found
Solvability for Generalized Applications
No full textSolvability is a key notion in the theory of call-by-name lambda-calculus, used in particular to identify meaningful terms. However, adapting this notion to other call-by-name calculi, or extending it to different models of computation - such as call-by-value - , is not straightforward. In this paper, we study solvability for call-by-name and call-by-value lambda-calculi with generalized applications, both variants inspired from von Plato’s natural deduction with generalized elimination rules. We develop an operational as well as a logical theory of solvability for each of them. The operational characterization relies on a notion of solvable reduction for generalized applications, and the logical characterization is given in terms of typability in an appropriate non-idempotent intersection type system. Finally, we show that solvability in generalized applications and solvability in the lambda-calculus are equivalent notions
Front Matter, Table of Contents, Preface, Steering Committee, Program Committee, External Reviewers, Organising Commitee
No full textFront Matter, Table of Contents, Preface, Steering Committee, Program Committee, External Reviewers, Organising Commite
Types as Resources for Classical Natural Deduction
No full textWe define two resource aware typing systems for the lambda-mu-calculus based on non-idempotent intersection and union types. The
non-idempotent approach provides very simple combinatorial arguments - based on decreasing measures of type derivations - to characterize head and strongly normalizing terms. Moreover, typability provides upper bounds for the length of head-reduction sequences and maximal reduction sequences
Encoding Tight Typing in a Unified Framework
No full textThis paper explores how the intersection type theories of call-by-name (CBN) and call-by-value (CBV) can be unified in a more general framework provided by call-by-push-value (CBPV). Indeed, we propose tight type systems for CBN and CBV that can be both encoded in a unique tight type system for CBPV. All such systems are quantitative, i.e. they provide exact information about the length of normalization sequences to normal form as well as the size of these normal forms. Moreover, the length of reduction sequences are discriminated according to their multiplicative and exponential nature, a concept inherited from linear logic. Last but not least, it is possible to extract quantitative measures for CBN and CBV from their corresponding encodings in CBPV
A Strong Bisimulation for a Classical Term Calculus
No full textWhen translating a term calculus into a graphical formalism many inessential details are abstracted away. In the case of -calculus translated to proof-nets, these inessential details are captured by a notion of equivalence on -terms known as -equivalence, in both the intuitionistic (due to Regnier) and classical (due to Laurent) cases. The purpose of this paper is to uncover a strong bisimulation behind -equivalence, as formulated by Laurent for Parigot\u27s -calculus. This is achieved by introducing a relation , defined over a revised presentation of -calculus we dub .
More precisely, we first identify the reasons behind Laurent\u27s -equivalence on -terms failing to be a strong bisimulation. Inspired by Laurent\u27s \emph{Polarized Proof-Nets}, this leads us to distinguish multiplicative and exponential reduction steps on terms. Second, we enrich the syntax of to allow us to track the exponential operations. These technical ingredients pave the way towards a strong bisimulation for the classical case. We introduce a calculus and a relation that we show to be a strong bisimulation with respect to reduction in , ie. two -equivalent terms have the exact same reduction semantics, a result which fails for Regnier\u27s -equivalence in -calculus as well as for Laurent\u27s -equivalence in . Although is formulated over an enriched syntax and hence is not strictly included in Laurent\u27s , we show how it can be seen as a restriction of it.arXiv admin note: text overlap with arXiv:1906.0937
Node Replication: Theory And Practice
No full textWe define and study a term calculus implementing higher-order node replication. It is used to specify two different (weak) evaluation strategies: call-by-name and fully lazy call-by-need, that are shown to be observationally equivalent by using type theoretical technical tools
A Faithful and Quantitative Notion of Distant Reduction for the Lambda-Calculus with Generalized Applications
No full textWe introduce a call-by-name lambda-calculus with generalized applications which is equipped with distant reduction. This allows to unblock -redexes without resorting to the standard permutative conversions of generalized applications used in the original -calculus with generalized applications of Joachimski and Matthes. We show strong normalization of simply-typed terms, and we then fully characterize strong normalization by means of a quantitative (i.e. non-idempotent intersection) typing system. This characterization uses a non-trivial inductive definition of strong normalization --related to others in the literature--, which is based on a weak-head normalizing strategy. We also show that our calculus relates to explicit substitution calculi by means of a faithful translation, in the sense that it preserves strong normalization. Moreover, our calculus and the original -calculus determine equivalent notions of strong normalization. As a consequence, inherits a faithful translation into explicit substitutions, and its strong normalization can also be characterized by the quantitative typing system designed for , despite the fact that quantitative subject reduction fails for permutative conversions
Front Matter, Table of Contents, Preface, Conference Organization
No full textFront Matter, Table of Contents, Preface, Conference Organizatio
LIPIcs, Volume 269, TYPES 2022, Complete Volume
No full textLIPIcs, Volume 269, TYPES 2022, Complete Volum
- …
