A Symmetric Lambda-Calculus Corresponding to the Negation-Free Bilateral Natural Deduction

TL;DR

This paper introduces a simple symmetric lambda-calculus aligned with negation-free bilateral natural deduction, deriving function duality from bilateralism rather than assuming it, and includes a call-value calculus for duality justification.

Contribution

It proposes a new symmetric lambda-calculus based on negation-free bilateralism, deriving function duality from proof-theoretic principles rather than assuming it.

Findings

Mutual transformations between expressions and continuations are definable.

Every typable function has dual types.

The calculus includes a call-value calculus for duality justification.

Abstract

Filinski constructed a symmetric lambda-calculus consisting of expressions and continuations which are symmetric, and functions which have duality. In his calculus, functions can be encoded to expressions and continuations using primitive operators. That is, the duality of functions is not derived in the calculus but adopted as a principle of the calculus. In this paper, we propose a simple symmetric lambda-calculus corresponding to the negation-free natural deduction based bilateralism in proof-theoretic semantics. In our calculus, continuation types are represented as not negations of formulae but formulae with negative polarity. Function types are represented as the implication and but-not connectives in intuitionistic and paraconsistent logics, respectively. Our calculus is not only simple but also powerful as it includes a call-value calculus corresponding to the call-by-value dual calculus invented by Wadler. We show that mutual transformations between expressions and continuations are definable in our calculus to justify the duality of functions. We also show that every typable function has dual types. Thus, the duality of function is derived from bilateralism.