File(s) not publicly available
Gödel’s System T Revisited
The linear lambda calculus, where variables are restricted to occur in terms exactly once, has a very weak expressive power: in particular, all functions terminate in linear time. In this paper we consider a simple extension with natural numbers and a restricted iterator: only closed linear functions can be iterated. We show properties of this linear version of Gödel’s T using a closed reduction strategy, and study the class of functions that can be represented. Surprisingly, this linear calculus offers a huge increase in expressive power over previous linear versions of T, which are ‘closed at construction’ rather than ‘closed at reduction’. We show that a linear T with closed reduction is as powerful as View the MathML source.
History
Publication status
- Published
Journal
Theoretical Computer ScienceISSN
03043975Publisher
ElsevierExternal DOI
Issue
11-13Volume
411Page range
1484-1500Department affiliated with
- Informatics Publications
Full text available
- No
Peer reviewed?
- Yes
Legacy Posted Date
2012-02-06Usage metrics
Categories
No categories selectedKeywords
Licence
Exports
RefWorks
BibTeX
Ref. manager
Endnote
DataCite
NLM
DC