2012/07/30 by Ali Assaf, Simon Perdrix · 4 citations
Computer Science · Mathematics · Physics and Astronomy · #Advanced Database Systems and Queries #Algebra over a field #Algebraic extension #Algebraic number #Calculus (dental) #Church encoding #Completeness (order theory) #Computer science #Connection (principal bundle) #Differential calculus #Differential equation #Discrete mathematics #Extension (predicate logic) #Geometry #Lambda #Lambda calculus #Logic, Reasoning, and Knowledge #Logic, programming, and type systems #Mathematical analysis #Mathematics #Physics #Programming language #Pure mathematics #Simply typed lambda calculus #Typed lambda calculus #cs.LO #quant-ph
paper · pdf · doi:10.4204/eptcs.88.2
published in Electronic Proceedings in Theoretical Computer Science 88, 16-27 (Open Publishing Association) · In Proceedings DCM 2011, arXiv:1207.6821
openalex publication_date 2012/07/30 · arxiv created 2012/07/31 · arxiv updated 2012/08/01 · openalex created_date 2025/10/10 · openalex updated_date 2026/08/06
The algebraic lambda calculus and the linear algebraic lambda calculus are two extensions of the classical lambda calculus with linear combinations of terms. They arise independently in distinct contexts: the former is a fragment of the differential lambda calculus, the latter is a candidate lambda calculus for quantum computation. They differ in the handling of application arguments and algebraic rules. The two languages can simulate each other using an algebraic extension of the well-known call-by-value and call-by-name CPS translations. These simulations are sound, in that they preserve reductions. In this paper, we prove that the simulations are actually complete, strengthening the connection between the two languages.