
Sign up to save your podcasts
Or


Commuting conversions are transformations on proofs in natural deduction, that move certain stuck inferences out of the way, so that the normal detour reductions (which correspond to beta-reduction under Curry-Howard) are enabled. The stuck inferences are uses of disjunction elimination. In programming terms, if you have an if-then-else (a simple case of or-elimination) where the then- and else-branches are lambda abstractions, and you apply that if-then-else to an argument, you need commuting conversions to move the argument into the branches, so you can call the functions (in the then- and else-branches) with it.
See Section 10.1 of Girard's Proofs and Types for more on the problem, and a nice paper by de Groote on strong normalization with commuting conversions.
By Aaron Stump5
1919 ratings
Commuting conversions are transformations on proofs in natural deduction, that move certain stuck inferences out of the way, so that the normal detour reductions (which correspond to beta-reduction under Curry-Howard) are enabled. The stuck inferences are uses of disjunction elimination. In programming terms, if you have an if-then-else (a simple case of or-elimination) where the then- and else-branches are lambda abstractions, and you apply that if-then-else to an argument, you need commuting conversions to move the argument into the branches, so you can call the functions (in the then- and else-branches) with it.
See Section 10.1 of Girard's Proofs and Types for more on the problem, and a nice paper by de Groote on strong normalization with commuting conversions.

288 Listeners

4,162 Listeners

7,255 Listeners

577 Listeners

561 Listeners

16,536 Listeners

14 Listeners

29 Listeners

69 Listeners