Lazy variable-renumbering makes substitution cheap

DOI10.1016/0020-0190(88)90114-7MaRDI QIDQ1114386zbMATH OpenOpenAlexFDO

Authors H. J. Boom

Publication date 1988

Published in Information Processing Letters (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/0020-0190(88)90114-7

zbMATH Keywords

data structureDe Bruijn numberlambda calculussubstitutionsymbol manipulationvariable capture

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40) Data structures (68P05) Symbolic computation and algebraic computation (68W30)

Review text

A new data structure for expressions with many variable bindings is efficient for symbol manipulation involving repeated complex substitution because it avoids making many trivially different copies. It retains variables, permits efficient alpha- and beta-conversion, and is appropriate for program transformation and formal logic.

Recommendations

• Substitution in non-wellfounded syntax with variable binding
• Substitution in non-wellfounded syntax with variable binding
• The soundness of explicit substitution with nameless variables
• Lazy call-by-value evaluation
• scientific article; zbMATH DE number 1500649
• Optimization by non-deterministic, lazy rewriting
• Lazy rewriting and context-sensitive rewriting
• A (Somewhat) New Solution to the Variable Binding Problem
• Lazy rewriting and eager machinery

Cites work

• scientific article; zbMATH DE number 3692654 (Why is no real title available?)
• scientific article; zbMATH DE number 194911 (Why is no real title available?)
• The lambda calculus. Its syntax and semantics. Rev. ed.

Cited in

(1)

• Efficient substitution in Hoare logic expressions

This page was built for publication: Lazy variable-renumbering makes substitution cheap

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1114386)