Rules for sequent calculus connectives, formatted as a cheat sheet. Additive Multiplicative Implicative Negation Assertion Shifts Quantification Core Structural - + Additive 1 A A B 2 B A B , A , B , A B A , B , A B , A A B 1 B A B 2 ( A B ) ≈ A B ( A B ) ≈ A B no left rule for , , no right rule for ≈ ≈ Multiplicative A B A B , A , B , A B A , B , A B , A B A B ( A B ) ≈ A B ( A B ) ≈ A B R R R R…
The Curry-Howard correspondence is a map for moving between logic and type theory, relating propositions with types and proofs with programs. It describes a two-way street, and we can freely move between the two worlds, or perhaps merely two perspectives , so long as we follow the map. Sometimes the road takes us to unexpected places. Here’s a trip I’ve been on recently. Double negation I’ve been…
Sequent calculi are powerful and flexible tools for studying logic and, via Curry-Howard, computation. But why, and how? Where does this power come from? We enjoy a variety of idioms to describe the relationship between problems and solutions. For example: “use the right tool for the job,” and “a good impedance match.” Where sequent calculi offer a good impedance match, it may in part be because…
Functions of type A → B can be translated into corresponding functions of type ¬B → ¬A in continuation-passing style (CPS), where ¬A is logically negation but computationally a continuation from A. This widens the view of functions as value transformers, taking values of type A to values of type B, to include an alternative perspective of them as continuation transformers (as noted by Andrzej…
The rules for a variety of polarized classical connectives, in a focused sequent calculus presentation to reflect a variety of dualities, and interpreted via Curry-Howard. Additive 1 A A B 2 B A B , A , B , A B & (“with”): negative conjunction ≈ lazy pair A , B , A B , A A B 1 B A B 2 ⊕ (“sum”): positive disjunction ≈ either ( A B ) ≈ A B ( A B ) ≈ A B The additive connectives, & (pronounced…
Nearly a century ago, Alonzo Church invented the simple, elegant, and yet elusive lambda calculus. Along with Alan Turing, he then proved the Church-Turing thesis: that anything computable with a Turing machine can also be computed in the lambda calculus. However, nearly as soon as we had digital computers, we started inventing programming languages, and with them a vast treasure of features,…
Swift’s value types are almost able to represent algebraic data types. Unfortunately, they fall short of the mark when it comes to recursion, and while they’ve announced that their solution, indirect case s, will ship in a later build of Swift 2, there’s still reason to want them today. The standard solution is to use Box<T> , a function, or some other reference type to manually force an…
Inscribe the orbit of Neptune in a square. Now, take a pair of integers as x and y coordinates across this square. Their size in bits determines the resolution at which they can measure this square. An integer of n bits can hold any of 2 ⁿ distinct values. 32-bit integers, therefore, would divide the square into a grid of 2³² points. At 32 bits of resolution, adjacent coordinates, e.g. … 0101 and…