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 Tools annual

Global: Zendy Free Plan

Global: Zendy Tools monthly

Global: Zendy Plus monthly

We introduce a call-by-name lambda-calculus    $$\lambda J$$  λ J with generalized applications which integrates a notion of distant reduction that allows to unblock    $$\beta $$  β -redexes without resorting to the permutative conversions of generalized applications. We show strong normalization of simply typed terms, and we then fully characterize strong normalization by means of a quantitative typing system. This characterization uses a non-trivial inductive definition of strong normalization –that we relate to others in the literature–, which is based on a weak-head normalizing strategy. Our calculus relates to explicit substitution calculi by means of a translation between the two formalisms which is faithful, in the sense that it preserves strong normalization. We show that our calculus    $$\lambda J$$  λ J and the well-know calculus    $$\varLambda J$$  Λ J determine equivalent notions of strong normalization. As a consequence,    $$\varLambda J$$  Λ J inherits a faithful translation into explicit substitutions, and its strong normalization can be characterized by the quantitative typing system designed for    $$\lambda J$$  λ J , despite the fact that quantitative subject reduction fails for permutative conversions.

A Faithful and Quantitative Notion of Distant Reduction for Generalized Applications