An equivalence between lambda- terms (Q1322165): Difference between revisions

\(\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.