Public
- Public
- Network
- Groups
- Featured
- Popular
- People

Conversation

Notices

Embed this notice
maonu (maonu@mathstodon.xyz)'s status on Friday, 13-Dec-2024 01:42:06 JST maonu

dialectica puts counter-witnesses where modus ponens (aka cut elimination, \( \beta \)-reduction is...
differential dialectica shows the chain rule in the same place!
Lots of depth in this work
https://inria.hal.science/hal-04583978/document
In conversation about 2 months ago from mathstodon.xyz permalink
Attachments
1. 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.
  https://media.mathstodon.xyz/media_attachments/files/113/625/924/634/154/076/original/480d9ac47d5b92ef.png

Feeds