An equivalence between lambda- terms
type: Item
instance of: scholarly article
title: An equivalence between lambda- terms
zbMATH Open document ID: 0801.03013
DOI: 10.1016/0304-3975(94)90012-4
author: Laurent Regnier
published in: Theoretical Computer Science
publication date: 1994-06-09T00:00:00Z
review text: \(\sigma\)-equivalence, which identifies terms differing only by permutation of radices, arises naturally from a translation of \(\lambda\)- terms into nets obtained by V. Danos and the author. This relation is given here a (simple) definition in the usual \(\lambda\)-calculus setting and it is proved that two \(\sigma\)-equivalent terms have the same normal form, if any, and the same operational behaviour with respect to the various reduction strategies (head, left, perpetual). It is also shown that the associated notion of \(\sigma\)-canonical form may be used to simplify case analysis when proving syntactical properties; this is applied to give a generalization of the perpetual strategy theorem.
Mathematics Subject Classification ID: 03B40
zbMATH DE Number: 562578
zbMATH Keywords: lambda calculus
zbMATH Keywords: operational properties of lambda-terms
zbMATH Keywords: sigma- equivalence
zbMATH Keywords: perpetual strategy
reviewed by: Chantal Berline
MaRDI profile type: Publication
full work available at URL: 0304-3975(94)90012-4
OpenAlex ID: W2008868842
cites work: Q3342534
cites work: Linear logic
cites work: Q3997016
description: scientific article; zbMATH DE number 562578