• Public

  • Public
  • Network
  • Groups
  • Featured
  • Popular
  • People

This is why the authors introduced a new reduction rule for this differential application: The newly introduced 𝜕𝑡/𝜕𝑧 · 𝑢 is called the linear substitution of 𝑧 by 𝑢 in 𝑡. Just like the usual substitution, linear substitution is a meta-theoretical operation defined by induction on 𝑡. Contrarily to the former, it only replaces a single linear occurrence of 𝑧 in 𝑡. As a result, not all occurrences of 𝑧 are replaced at the same time, hence 𝑧 may still be free in 𝜕𝑡/𝜕𝑧 · 𝑢, and thus 𝐷 (𝜆𝑧.𝑡) · 𝑢 reduces to a 𝜆-abstraction that binds 𝑧. We now detail the syntax and operational semantics of this calculus.