An equivalence between lambda- terms
\(\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.
- A notation for lambda terms. A generalization of environments
- Perpetual reductions in -calculus
- Strong normalization from weak normalization in typed \(\lambda\)-calculi
- Strong normalization through intersection types and memory
- De Bruijn's syntax and reductional behaviour of \(\lambda\)-terms: The typed case
- De Bruijn's syntax and reductional behaviour of \(\lambda\)-terms: the untyped case
- Polarized proof-nets and \(\lambda \mu\)-calculus
- Evaluating lambda terms with traversals
- The bang calculus revisited
- A note on discriminability of lambda terms
- Classical by-need
- The permutative -calculus
- Intersection types for the resource control lambda calculi
- Open call-by-value
- scientific article; zbMATH DE number 4179330 (Why is no real title available?)
- Revisiting call-by-value Böhm trees in light of their Taylor expansion
- An Operational Account of Call-by-Value Minimal and Classical λ-Calculus in “Natural Deduction” Form
- Monadic Translation of Intuitionistic Sequent Calculus
- scientific article; zbMATH DE number 1231514 (Why is no real title available?)
- A resource aware semantics for a focused intuitionistic calculus
- Linear -reduction
- Towards a semantic measure of the execution time in call-by-value lambda-calculus
- Head reduction and normalization in a call-by-value lambda-calculus
- Intuitionistic differential nets and lambda-calculus
- Effective longest and infinite reduction paths in untyped λ-calculi
- On the longest perpetual reductions in orthogonal expression reduction systems
- Extensional proofs in a propositional logic modulo isomorphisms
- The bang calculus revisited
- A faithful and quantitative notion of distant reduction for generalized applications
- A short proof that adding some permutation rules to \(\beta \) preserves SN
- A note on preservation of strong normalisation in the \(\lambda \)-calculus
- A strong bisimulation for a classical term calculus
- A faithful and quantitative notion of distant reduction for the lambda-calculus with generalized applications
- Factorize factorization
- Meaningfulness and genericity in a subsuming framework (invited talk)
- Resource operators for \(\lambda\)-calculus
- Proof nets and the call-by-value \(\lambda\)-calculus
- An exact correspondence between a typed pi-calculus and polarised proof-nets
This page was built for publication: An equivalence between lambda- terms
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1322165)
