gavrilovmiroslav / mae Goto Github PK

A Taste of Linear Logic by Philip Wadler

Tags: linear logic, explicit curry-howard

Traditional logic has close ties to computing in general and functional languages in particular. The Curry-Howard isomorphism specifies a precise correspondence between intuitionistic logic, on the one hand, and typed lambda calculus, on the other.

Traditional logic also encourages reckless use of resources, as the truth is indeed free. Linear logic comes in to fix this, allowing us to use only what is introduced, and only once. The two rules that change drastically are Contraction and Weakening, but instead of completely removing them (which would be too strict), we introduce a context for intuitionistic operations, and another for linear ones. This way, we can embed intuitionistic logic inside linear logic programs, as working without them makes the system too simple and allows some illegal proofs under proof reductions.