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

Categorical combinators [Curien 1986/1993; Hardin 1989; Yokouchi 1989] and more recently &lgr;&sgr;-calculus [Abadi 1991; Hardin and Le´vy 1989], have been introduced to provide an explicit treatment of substitutions in the &lgr;-calculus. We reintroduce here the ingredients of these calculi in a self-contained and stepwise way, with a special emphasis on confluence properties. The main new results of the paper with respect to Curien [1986/1993], Hardin [1989], Abadi [1991], and Hardin and Le´vy [1989] are the following:(1) We present a confluent weak calculus of substitutions, where no variable clashes can be feared;(2) We solve a conjecture raised in Abadi [1991]: &lgr;&sgr;-calculus is not confluent (it is confluent on ground terms only).This unfortunate result is “repaired” by presenting a confluent version of &lgr;&sgr;-calculus, named the &lgr;Env-caldulus in Hardin and Le´vy [1989], called here the confluent &lgr;&sgr;-calculus.

Confluence properties of weak and strong calculi of explicit substitutions