Perpetual reductions in \(\lambda\)-calculus

DOI10.1006/INCO.1998.2750zbMath0920.03024OpenAlexW2130554190MaRDI QIDQ1286373

Hongwei Xi, Femke van Raamsdonk, Morten Heine B. Sørensen, Paula G.Severi

Publication date: 9 September 1999

Published in: Information and Computation (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1006/inco.1998.2750

zbMATH Keywords

survey\(\lambda\)-calculustype theoryperpetual reductions\(\beta\)-reductioninfinite reduction pathsperpetual redexes

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40)

Related Items (18)

A type assignment for \(\lambda\)-calculus complete both for FPTIME and strong normalization ⋮ Unnamed Item ⋮ Quantitative weak linearisation ⋮ A note on preservation of strong normalisation in the \(\lambda \)-calculus ⋮ Tight typings and split bounds, fully developed ⋮ Polarised subtyping for sized types ⋮ On strong normalization and type inference in the intersection type discipline ⋮ On randomised strategies in the \(\lambda \)-calculus ⋮ Continuous normalization for the lambda-calculus and Gödel's T ⋮ Non-strictly positive fixed points for classical natural deduction ⋮ On the longest perpetual reductions in orthogonal expression reduction systems ⋮ Strong cut-elimination in sequent calculus using Klop's ι-translation and perpetual reductions ⋮ Strong Normalisation of Cut-Elimination That Simulates β-Reduction ⋮ Weak linearization of the lambda calculus ⋮ A Knuth-Bendix-like ordering for orienting combinator equations ⋮ Perpetuality and uniform normalization in orthogonal rewrite systems ⋮ Conservation and uniform normalization in lambda calculi with erasing reductions ⋮ Normalization for the Simply-Typed Lambda-Calculus in Twelf

Uses Software

• Automath

Cites Work

• On termination and confluence properties of disjoint and constructor-sharing conditional rewrite systems
• Reduction of higher type levels by means of an ordinal analysis of finite terms
• The lambda calculus. Its syntax and semantics. Rev. ed.
• Needed reduction and spine strategies for the lambda calculus
• BCK-combinators and linear \(\lambda\)-terms have types
• Lambda-calculus terms that reduce to themselves
• Church-Rosser strategies in the lambda calculus
• An equivalence between lambda- terms
• Selected papers on AUTOMATH, dedicated to N. G. de Bruijn
• Strong normalization from weak normalization in typed \(\lambda\)-calculi
• Strong normalization in type systems: A model theoretical approach
• An upper bound for reduction sequences in the typed \(\lambda\)-calculus
• Discrete Normalization and Standardization in Deterministic Residual Structures
• A direct proof of the finite developments theorem
• The Standardization Theorem for λ‐Calculus
• Ordinal analysis of terms of finite type
• Reductions of Residuals are Finite
• Finite family developments
• A general method for proving the normalization theorem for first and second order typed λ-calculi
• Optimal normalization in orthogonal term rewriting systems
• Polynomial time termination and constraint satisfaction tests
• A Note on Shortest Developments
• Intensional interpretations of functionals of finite type I
• Some Properties of Conversion
• Effective longest and infinite reduction paths in untyped λ-calculi
• Parallel reductions in \(\lambda\)-calculus
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Perpetual reductions in \(\lambda\)-calculus