We gratefully acknowledge support from
the Simons Foundation and member institutions.
Full-text links:

Download:

Current browse context:

cs.LO

Change to browse by:

cs

References & Citations

DBLP - CS Bibliography

Bookmark

(what is this?)
CiteULike logo BibSonomy logo Mendeley logo del.icio.us logo Digg logo Reddit logo ScienceWISE logo

Computer Science > Logic in Computer Science

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

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.
Subjects: Logic in Computer Science (cs.LO)
Cite as: arXiv:2101.12607 [cs.LO]
  (or arXiv:2101.12607v1 [cs.LO] for this version)

Submission history

From: Daisuke Kimura [view email]
[v1] Fri, 29 Jan 2021 14:39:29 GMT (74kb)

Link back to: arXiv, form interface, contact.