Gödel’s System T Revisited

Mackie, Ian (2010) Gödel’s System T Revisited. Theoretical Computer Science, 411 (11-13). pp. 1484-1500. ISSN 03043975

Full text not available from this repository.


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.

Item Type: Article
Schools and Departments: School of Engineering and Informatics > Informatics
Depositing User: Ian Mackie
Date Deposited: 06 Feb 2012 18:40
Last Modified: 31 May 2012 11:38
URI: http://sro.sussex.ac.uk/id/eprint/17718
📧 Request an update