English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

We address a problem connected to the unfolding semantics of functionalprogramming languages: give a useful characterization of those infinitelambda-terms that are lambda_{letrec}-expressible in the sense that they ariseas infinite unfoldings of terms in lambda_{letrec}, the lambda-calculus withletrec. We provide two characterizations, using concepts we introduce forinfinite lambda-terms: regularity, strong regularity, and binding-capturingchains. It turns out that lambda_{letrec}-expressible infinite lambda-termsform a proper subclass of the regular infinite lambda-terms. In this paper weestablish these characterizations only for expressibility in lambda_{mu}, thelambda-calculus with explicit mu-recursion. We show that for all infinitelambda-terms T the following are equivalent: (i): T is lambda_{mu}-expressible;(ii): T is strongly regular; (iii): T is regular, and it only has finitebinding-capturing chains.  We define regularity and strong regularity for infinite lambda-terms as twodifferent generalizations of regularity for infinite first-order terms: as theexistence of only finitely many subterms that are defined as the reducts of tworewrite relations for decomposing lambda-terms. These rewrite relations act oninfinite lambda-terms furnished with a marked prefix of abstractions forcollecting decomposed lambda-abstractions and keeping the terms closed underdecomposition. They differ in how vacuous abstractions in the prefix areremoved.  This report accompanies the article with the same title for the proceedingsof the conference RTA 2013, and mainly differs from that by providing the proofof the characterization of lambda_{mu}-expressibility with binding-capturingchains.

Expressibility in the Lambda Calculus with mu