Normal-order reduction grammars

DOI10.1017/S0956796816000332MaRDI QIDQ5372004zbMATH OpenOpenAlexFDO

Authors Maciej Bendkowski

Publication date 23 October 2017

Published in Journal of Functional Programming (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1603.01758

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40) Grammars and rewriting systems (68Q42)

Abstract: We present an algorithm which, for given $n$, generates an unambiguous regular tree grammar defining the set of combinatory logic terms, over the set $S,K$ of primitive combinators, requiring exactly $n$ normal-order reduction steps to normalize. As a consequence of Curry and Feys's standardization theorem, our reduction grammars form a complete syntactic characterization of normalizing combinatory logic terms. Using them, we provide a recursive method of constructing ordinary generating functions counting the number of $SK$-combinators reducing in $n$ normal-order reduction steps. Finally, we investigate the size of generated grammars, giving a primitive recursive upper bound.

Recommendations

• Complexity of normal form grammars
• Publication:3485873
• scientific article; zbMATH DE number 4053048
• Parameter-reduction of higher level grammars
• scientific article; zbMATH DE number 4112043
• Normal forms for phrase-structure grammars
• scientific article; zbMATH DE number 4189198
• scientific article; zbMATH DE number 4131693
• On normal form grammars and their size
• scientific article; zbMATH DE number 1452979

Cites work

• A natural counting of lambda terms
• A new implementation technique for applicative languages
• Analytic combinatorics
• Asymptotic properties of combinatory logic
• Asymptotically almost all \lambda-terms are strongly normalizing
• Boltzmann Samplers for the Random Generation of Combinatorial Structures
• Counting and generating lambda terms
• Counting and generating terms in the binary lambda calculus
• scientific article; zbMATH DE number 3863589 (Why is no real title available?)
• Non-idempotent intersection types and strong normalisation
• On the number of lambda terms with prescribed size of their de Bruijn representation
• The lambda calculus. Its syntax and semantics. Rev. ed.

Cited in

(7)

• Parameter-reduction of higher level grammars
• The combinator S
• On the likelihood of normalization in combinatory logic
• On the enumeration of closures and environments with an application to random generation
• Counting environments and closures
• Towards the average-case analysis of substitution resolution in \(\lambda\)-calculus
• scientific article; zbMATH DE number 4189198 (Why is no real title available?)

Describes a project that uses

Uses Software

• Miranda

This page was built for publication: Normal-order reduction grammars

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