<abstract xmlns="http://www.w3.org/1999/xhtml">

<p>Leveraging our recent work on the enumeration of <italic>β</italic>-redices in closed linear λ-terms, we present an algorithm for sampling <italic>β</italic>-normal closed linear λ-terms and their corresponding maps. Such terms correspond to proofs of tautologies in implicational linear logic and their generation is of interest in various domains, including the testing of linear logic theorem provers.</p>
</abstract>

Leveraging our recent work on the enumeration of β-redices in closed linear λ-terms, we present an algorithm for sampling β-normal closed linear λ-terms and their corresponding maps. Such terms correspond to proofs of tautologies in implicational linear logic and their generation is of interest in various domains, including the testing of linear logic theorem provers.

Sampling <italic>β</italic>-normal linear λ-terms

Pure Mathematics and Applications

This work is licensed under the Creative Commons Attribution-NonCommercial-NoDerivatives 3.0 License.

{"article-title":{"italic":"β","content":["Sampling","-normal linear λ-terms"]}}

Leveraging our recent work on the enumeration of β-redices in closed linear λ-terms, we present an algorithm for sampling β-normal closed linear λ-terms and...

Sampling β-normal linear λ-terms

Published Online: Jun 18, 2022

Page range: 45 - 55

Received: Mar 31, 2022

Accepted: May 15, 2022

DOI: https://doi.org/10.2478/puma-2022-0008

Keywords
lambda-calculus, cubic map, random generation, linear logic

© 2022 Olivier Bodini et al., published by Sciendo

This work is licensed under the Creative Commons Attribution-NonCommercial-NoDerivatives 3.0 License.

Sampling β-normal linear λ-terms

Published Online: Jun 18, 2022

Page range: 45 - 55

Received: Mar 31, 2022

Accepted: May 15, 2022

DOI: https://doi.org/10.2478/puma-2022-0008

Keywordslambda-calculus, cubic map, random generation, linear logic

© 2022 Olivier Bodini et al., published by Sciendo

This work is licensed under the Creative Commons Attribution-NonCommercial-NoDerivatives 3.0 License.

Keywords
lambda-calculus, cubic map, random generation, linear logic