The insensitivity theorem for nonreducing reflexive types
type: Item
instance of: scholarly article
title: The insensitivity theorem for nonreducing reflexive types
zbMATH Open document ID: 0537.68035
DOI: 10.1016/0022-0000(83)90049-1
author: Egidio Astesiano
author: Gerardo Costa
published in: Journal of Computer and System Sciences
publication date: 1983-01-01T00:00:00Z
review text: The paper is concerned to the problem of deciding which are the useful types for typed \(\lambda\)-expression programming languages (ALGOL 68, LISP, etc.). In the first section the authors present the concept of reducing type and their hierarchies of finite and infinite types. In a previous paper by the authors [Lect. Notes Comput. Sci. 85, 38-50 (1980; Zbl 0444.68026)], they showed that the nonreducing types are useless for primitive functions of first order type and for terms having the same meaning if they behave in the same way in any program (fully abstract semantics). This result comes from a more general and stronger syntactic result, obtained in the present paper (Insensitivity Theorem): contexts of finite type and closed with respect to variables of reflexive type are insensitive to differences between terms of nonreducing type. Formally, the theorem is the following: if \(M^ 1\), \(M^ 2\) are two terms of the same nonreducing type, C[] a context for them and \(C[M^ 1]\), \(C[M^ 2]\) are i-closed terms of finite type, then \(val(C[M^ 1])=val(C[M^ 2])\) (val denoting the ''syntactic'' value of a term). A main consequence is that nonreducing types are useless within a fully abstract semantics. The third section illustrates the role played by the concept of reducing type in applicative language modelling. Semantics (defined by models) and full abstraction concepts are introduced and the insensitivity theorem related to a new programming languages design principle. Finally, hints about further researches on this topic are given.
Mathematics Subject Classification ID: 68Q65
Mathematics Subject Classification ID: 68Q60
Mathematics Subject Classification ID: 03D65
Mathematics Subject Classification ID: 03B40
Mathematics Subject Classification ID: 03D55
Mathematics Subject Classification ID: 03B15
zbMATH DE Number: 3854408
zbMATH Keywords: typed lambda calculus
zbMATH Keywords: free continuous algebras
zbMATH Keywords: programming languages
zbMATH Keywords: reducing type
zbMATH Keywords: abstract semantics
zbMATH Keywords: applicative language modelling
reviewed by: Neculai Curteanu
describes a project that uses: ALGOL 68
MaRDI profile type: Publication
full work available at URL: 0022-0000(83)90049-1
OpenAlex ID: W2060254233
cites work: Q4139647
cites work: Q3888521
cites work: Q3954807
cites work: Initial Algebra Semantics and Continuous Algebras
cites work: Q4772711
cites work: Fully abstract models of typed \(\lambda\)-calculi
cites work: Data Types as Lattices
cites work: The Relation between Computational and Denotational Properties for Scott’s ${\text{D}}_\infty $-Models of the Lambda-Calculus
description: scientific article; zbMATH DE number 3854408