Soft Linear Set Theory |
| |
Authors: | Richard McKinley |
| |
Affiliation: | aTheoretische Informatik und Logik, Institut für Informatik und angewandte Mathematik, Neubrückstrasse 10, CH-3012 Bern, Switzerland |
| |
Abstract: | A formulation of naïve set theory is given in Lafont’s Soft Linear Logic, a logic with polynomial time cut-elimination. We demonstrate that the provably total functions of this set theory are precisely the PTIME functions. A novelty of this approach is the representation of the unary/binary natural numbers by two distinct sets (the safe naturals and the soft naturals). |
| |
Keywords: | |
本文献已被 ScienceDirect 等数据库收录! |
|