University of Sussex
Browse

File(s) not publicly available

Gödel’s System T Revisited

journal contribution
posted on 2023-06-07, 20:56 authored by Ian MackieIan Mackie
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 Science

ISSN

03043975

Publisher

Elsevier

Issue

11-13

Volume

411

Page range

1484-1500

Department affiliated with

  • Informatics Publications

Full text available

  • No

Peer reviewed?

  • Yes

Legacy Posted Date

2012-02-06

Usage metrics

    University of Sussex (Publications)

    Categories

    No categories selected

    Exports

    RefWorks
    BibTeX
    Ref. manager
    Endnote
    DataCite
    NLM
    DC