Deriving efficient sequential and parallel generators for closed simply-typed lambda terms and normal forms

DOI10.3233/FI-2020-1994MaRDI QIDQ4988930zbMATH OpenOpenAlexFDO

Authors Paul Tarau

Publication date 20 May 2021

Published in Fundamenta Informaticae (Search for Journal in Brave)

Full work available at URL https://doi.org/10.3233/fi-2020-1994

zbMATH Keywords

logic programming transformationsnormal formsparallel combinatorial generation algorithmsProlog multi-threadingsequential combinatorial generation algorithmssimply-typed lambda termstype inference

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40) Logic programming (68N17)

Recommendations

• A hiking trip through the orders of magnitude: deriving efficient generators for closed simply-typed lambda terms and normal forms
• Counting and generating lambda terms
• Random generation of closed simply typed λ-terms: A synergy between logic programming and Boltzmann samplers
• Quantitative Aspects of Linear and Affine Closed Lambda Terms
• Counting and generating terms in the binary lambda calculus

Cites work

• \(\lambda\) to SKI, semantically -- declarative pearl
• A hiking trip through the orders of magnitude: deriving efficient generators for closed simply-typed lambda terms and normal forms
• A natural counting of lambda terms
• Analytic combinatorics
• Asymptotically almost all \lambda-terms are strongly normalizing
• Binary lambda calculus and combinatory logic
• Counting and generating lambda terms
• Counting and generating terms in the binary lambda calculus
• Efficient generation of test data structures using constraint logic programming and program transformation
• scientific article; zbMATH DE number 5318491 (Why is no real title available?)
• Introduction to generalized type systems
• Intuitionistic propositional logic is polynomial-space complete
• Lambda terms of bounded unary height
• On uniquely closable and uniquely typable skeletons of lambda terms
• Random generation of closed simply typed λ-terms: A synergy between logic programming and Boltzmann samplers
• Ranking/unranking of lambda terms with compressed de Bruijn indices
• SWI-Prolog
• The full-reducing Krivine abstract machine KN simulates pure normal-order reduction in lockstep: a proof via corresponding calculus
• The lambda calculus. Its syntax and semantics. Rev. ed.
• The YAP prolog system
• Types for proofs and programs. International conference, TYPES 2007, Cividale des Friuli, Italy, May 2--5, 2007. Revised selected papers

Cited in

(3)

• On uniquely closable and uniquely typable skeletons of lambda terms
• A hiking trip through the orders of magnitude: deriving efficient generators for closed simply-typed lambda terms and normal forms
• Random generation of closed simply typed λ-terms: A synergy between logic programming and Boltzmann samplers

Describes a project that uses

Uses Software

• Automath
• OEIS

This page was built for publication: Deriving efficient sequential and parallel generators for closed simply-typed lambda terms and normal forms

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