Gödel's system T revisited

No Thumbnail Available
Date
2010
Authors
Ian Mackie
Sandra Alves
Maribel Fernández
Mário Florido
Journal Title
Journal ISSN
Volume Title
Publisher
Abstract
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 Godel'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 T.
Description
Keywords
Citation