General recursive functions in a very simply interpretable typed \(\lambda\)-calculus
type: Item
instance of: scholarly article
title: General recursive functions in a very simply interpretable typed \(\lambda\)-calculus
zbMATH Open document ID: 0796.03019
DOI: 10.1016/0304-3975(93)90088-B
author: G. Jacopini
author: Giovanna Sontacchi
published in: Theoretical Computer Science
publication date: 1994-10-09T00:00:00Z
review text: This paper is in the setting of simply typed lambda-calculus. It is well known that not all partial recursive functions can be represented in this system. The authors propose to add to the \(\lambda\)-calculus four constants and two reduction rules: the first two constants represent the zero and successor for type 0. The other two allow, using the new rules, the changes of types for integers which are necessary for dealing with primitive recursion and the \(\mu\)-operator. This results in a typed \(\lambda\)-calculus, where all partial recursive functions are represented. A model is provided, using simply a hierarchy of function spaces based upon an infinite base set. Finally a curious new extension with one more constant allows the description of some parallel operators.
reviewed by: N. Bernard
Mathematics Subject Classification ID: 03B40
Mathematics Subject Classification ID: 03D20
zbMATH DE Number: 501168
zbMATH Keywords: simply typed lambda-calculus
zbMATH Keywords: partial recursive functions
zbMATH Keywords: parallel operators
MaRDI profile type: Publication
cites work: A discrimination algorithm inside \(\lambda -\beta\)-calculus
cites work: Q4722037
cites work: LCF considered as a programming language
cites work: \(\mathbb{T}^\omega\) as a universal domain
Recommended article: Typed λ-calculus with recursive definitions
Recommended article: Simple general recursion in type theory
Recommended article: General Recursion via Coinductive Types
Recommended article: Q4435459
Recommended article: Q3138540
Recommended article: A user's friendly syntax to define recursive functions as typed λ-terms
Recommended article: Q3793765
Recommended article: Lambda calculus with explicit recursion
Recommended article: Q4790656
Recommended article: Q3745258
description: scientific article; zbMATH DE number 501168