Normal-order reduction grammars

DOI10.1017/S0956796816000332zbMATH Open1418.68111arXiv1603.01758OpenAlexW2964182341MaRDI QIDQ5372004FDOQ5372004

Maciej Bendkowski

Publication date: 23 October 2017

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

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.

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

Mathematics Subject Classification ID

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

Cites Work

• Title not available (Why is that?)
• Title not available (Why is that?)
• The lambda calculus. Its syntax and semantics. Rev. ed.
• Non-idempotent intersection types and strong normalisation
• Boltzmann Samplers for the Random Generation of Combinatorial Structures
• A new implementation technique for applicative languages
• Asymptotic Properties of Combinatory Logic
• A Natural Counting of Lambda Terms
• On the number of lambda terms with prescribed size of their De Bruijn representation
• Asymptotically almost all \lambda-terms are strongly normalizing
• Counting and generating terms in the binary lambda calculus
• Counting and generating lambda terms

Cited In (6)

• The combinator S
• Title not available (Why is that?)
• Title not available (Why is that?)
• Parameter-reduction of higher level grammars
• On the enumeration of closures and environments with an application to random generation
• Title not available (Why is that?)

Uses Software

• Miranda

   Recommendations

• Complexity of normal form grammars 👍 👎
• Title not available (Why is that?) 👍 👎
• Title not available (Why is that?) 👍 👎
• Parameter-reduction of higher level grammars 👍 👎
• Title not available (Why is that?) 👍 👎
• Normal forms for phrase-structure grammars 👍 👎
• Title not available (Why is that?) 👍 👎
• Title not available (Why is that?) 👍 👎
• ON NORMAL FORM GRAMMARS AND THEIR SIZE 👍 👎
• Title not available (Why is that?) 👍 👎

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)