Sökning: hsv:(NATURVETENSKAP) hsv:(Data och informationsvetenskap Datateknik) >
A type-assignment o...
A type-assignment of linear erasure and duplication
-
- Curzi, Gianluca, 1991 (författare)
- Gothenburg University,Göteborgs universitet,Institutionen för filosofi, lingvistik och vetenskapsteori,Department of Philosophy, Linguistics and Theory of Science
-
Roversi, Luca (författare)
-
(creator_code:org_t)
-
-
visa fler...
-
-
visa färre...
- 2020
- 2020
- Engelska.
-
Ingår i: Theoretical Computer Science. - 0304-3975.
- Relaterad länk:
-
https://gup.ub.gu.se...
Abstract
Ämnesord
Stäng
- We introduce ???, a type-assignment system for the linear λ-calculus that extends second-order ????2, i.e., intuitionistic multiplicative Linear Logic, by means of logical rules that weaken and contract assumptions, but in a purely linear setting. ??? enjoys both a mildly weakened cut-elimination, whose computational cost is cubic, and Subject reduction. A translation of ??? into ????2 exists such that the derivations of the former can exponentially compress the dimension of the derivations in the latter. ??? allows for a modular and compact representation of boolean circuits, directly encoding the fan-out nodes, by contraction, and disposing garbage, by weakening. It can also represent natural numbers with terms very close to standard Church numerals which, moreover, apply to Hereditarily Finite Permutations, i.e. a group structure that exists inside the linear λ-calculus.
Ämnesord
- NATURVETENSKAP -- Data- och informationsvetenskap (Datateknik) (hsv//swe)
- NATURAL SCIENCES -- Computer and Information Sciences (hsv//eng)
Nyckelord
- Second-order multiplicative linear logic
- Type-assignment
- Linear λ-calculus
- Cut-elimination (cost)
- Boolean circuits
- Numerals
- Hereditarily finite permutations
Publikations- och innehållstyp
- ref (ämneskategori)
- art (ämneskategori)
Hitta via bibliotek
Till lärosätets databas