Why Cut Elimination is More Complicated than Normalization
Iowa Type Theory Commute
English - October 05, 2021 05:00 - 12 minutes - 8.34 MB - ★★★★★ - 13 ratingsTechnology Science Mathematics programming languages computational logic type theory proof assistants cedille Homepage Download Apple Podcasts Google Podcasts Overcast Castro Pocket Casts RSS feed
Previous Episode: Introduction to Cut Elimination
Next Episode: Structural rules, or the Curse of the Bound Variable
Cut elimination for sequent calculus is more involved that normalization of detours for natural deduction. There are more cases of cuts that must be transformed than correspond to detours (introductions followed by eliminations). In this episode, I explain why that is.