Godel's system T revisited

TY - JOUR

T1 - Godel's system T revisited

AU - Alves, Sandra

AU - Fernandez, Maribel

AU - Florido, Mario

AU - Mackie, Ian

PY - 2010/3/6

Y1 - 2010/3/6

N2 - 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.

AB - 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.

U2 - 10.1016/j.tcs.2009.11.014

DO - 10.1016/j.tcs.2009.11.014

M3 - Article

VL - 411

SP - 1484

EP - 1500

JO - Theoretical Computer Science

JF - Theoretical Computer Science

IS - 11-13

ER -