A New Proof of P-time Completeness of Linear Lambda Calculus
Satoshi Matsuoka
TL;DR
This paper presents a novel proof demonstrating that Linear Lambda Calculus is P-time complete, utilizing a different Boolean type and enabling machine-checked verification of the proof.
Contribution
It introduces a new proof method for P-time completeness of Linear Lambda Calculus with an alternative Boolean type, facilitating automated correctness checking.
Findings
New proof of P-time completeness using different Boolean type
Proof can be verified by machine-checked implementation
Provides an alternative approach to Mairson's original proof
Abstract
We give a new proof of P-time completeness of Linear Lambda Calculus, which was originally given by H. Mairson in 2003. Our proof uses an essentially different Boolean type from the type Mairson used. Moreover the correctness of our proof can be machined-checked using an implementation of Standard ML.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, programming, and type systems · Formal Methods in Verification · semigroups and automata theory