An equivalence between lambda- terms (Q1322165): Difference between revisions
From MaRDI portal
Changed an Item |
Set profile property. |
||
Property / MaRDI profile type | |||
Property / MaRDI profile type: MaRDI publication profile / rank | |||
Normal rank |
Revision as of 02:56, 5 March 2024
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | An equivalence between lambda- terms |
scientific article |
Statements
An equivalence between lambda- terms (English)
0 references
9 June 1994
0 references
\(\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.
0 references
lambda calculus
0 references
operational properties of lambda-terms
0 references
sigma- equivalence
0 references
perpetual strategy
0 references