## Wednesday, January 30, 2008

### Fun with polarity and unicode

> Dependent pattern-matching and unicode: a killer combination.
> I will try to post more about this in the next few days.

"Few" is subjective.

Before getting to the Agda code that Dan and I wrote, though, I wanted to talk a little bit about a neat, simple idea I learned recently. In this paper, I argued that one way to rationally reconstruct the linear logic notion of polarity was to turn to so-called proof-theoretic semantics, and in particular Michael Dummett's distinction between verificationist and pragmatist justifications of the logical rules. A verificationist meaning-theory supposes that connectives are defined by their introduction rules, and uses this definition to justify their elimination rules. A pragmatist meaning-theory supposes the opposite: connectives are defined by their elimination rules, and this justifies their introduction rules. Well, polarity lets us refine this picture: the positive connectives are defined by their introduction rules, the negative connectives by their elimination rules.

But another (more fun?) way to think about polarity is through game-theoretic semantics. Think of the truth of a proposition A as a game between Prover and Refuter: A is valid iff Prover has a winning strategy. So the meaning of a connective is essentially a set of rules for playing a game. A few examples:

• [A ⊕ B] : This is a game where Prover begins by selecting either A or B, after which play proceeds by the rules of that game.

• [A & B] : This is a game where Refuter begins by selecting either A or B, after which play proceeds by the rules of that game.

• [A] : Play A, but with the roles of Prover and Refuter swapped.

•  : Prover begins but has no moves, so Refuter automatically wins.

• [⊤] : Refuter begins but has no moves, so Prover automatically wins.

The polarity of a connective/formula is just the answer to the important question: "Which player begins?" (By the way, this also gives another explanation for focus and inversion. Focus is just the fact that after making a move in the game A ⊕ B, Prover doesn't have to give up her turn to Refuter, e.g., A could itself be the game A₁⊕ A₂. Inversion is the fact that the second player really has no choice in the matter, e.g., in the game A ⊕ B, Refuter has to account for Prover playing either A or B.)

The reason I like this (I think pretty old) idea is that not only is it a good icebreaker at parties, but it also suggests a natural generalization, which Samson Abramsky (a bit tongue-in-cheek) calls Socially Responsive, Environmentally Friendly Logic. Rather than treating only 2-player games between Prover and Refuter, we can encode n-player games using n distinct polarities. For example, Abramsky defines the connective A ⊕α B as the game where α begins play, selecting between A and B. I think this is a really cool and promising generalization.

But anyways, today let's stick with the boring, bipolar world. I'm going to talk about how to give a focused encoding of polarized intuitionistic logic in Agda, which is simultaneously a deep embedding of a language with explicit evaluation order and pattern-matching. For those playing along, the full code is available here. Let's start with some boilerplate:

``open import Data.Listopen import Data.String renaming (_++_ to concat) module Main where``

Now we define the syntax of polarized formulas, as two mutually inductive datatypes.
``  module Types where    Atom : Set     Atom = String    mutual      data Pos : Set where        X⁺  : Atom -> Pos        ↓   : Neg -> Pos        1⁺  : Pos        _*_ : Pos -> Pos -> Pos        0⁺  : Pos        _+_ : Pos -> Pos -> Pos        2⁺ : Pos        ℕ  : Pos      data Neg : Set where        X- : Atom -> Neg        ↑ : Pos -> Neg        ⊤ : Neg        _→_ : Pos -> Neg -> Neg        _&_ : Neg -> Neg -> Neg      infixr 14 _→_      infixr 15 _&_      infixr 15 _+_      infixr 16 _*_``

Positive formulas include positive atoms and shifted negative formulas, as well as strict products and sums. (We would call the units 1 and 0, but unfortunately Agda doesn't let us overload numerical constants.) For fun, we also defined the type of booleans 2⁺, and the type of natural numbers ℕ. Negative formulas include negative atoms and shifted positive formulas, as well as functions and lazy products. Observe the essential use of Unicode!

Now we define hypotheses (positive atoms or arbitrary negative formulas) and conclusions (negative atoms or arbitrary positive formulas), as well as some simple machinery for inspecting contexts. Contexts are basically lists of hypotheses, but since inversion introduces multiple hypotheses at a time, it is more convenient to work with lists of lists of hypotheses. Hence we define LCtx (linear context) and UCtx (unrestricted context), and the membership relationships ∈ and ∈∈. Proofs of membership are isomorphic to De Bruijn indices.

``  module Contexts where    open Types public    data Hyp : Set where      HP : Atom -> Hyp      HN : Neg -> Hyp    data Conc : Set where      CP : Pos -> Conc      CN : Atom -> Conc    LCtx : Set    LCtx = List Hyp    UCtx : Set    UCtx = List LCtx    data _∈_ : Hyp -> LCtx -> Set where      f0 : {h : Hyp}   {Δ : LCtx} -> h ∈ (h :: Δ )      fS : {h h' : Hyp} {Δ : LCtx} -> h' ∈ Δ -> h' ∈ (h :: Δ)    data _∈∈_ : Hyp -> UCtx -> Set where      s0 : {h : Hyp} {Δ : LCtx} {Γ : UCtx} -> h ∈ Δ -> h ∈∈ (Δ :: Γ)      sS : {h : Hyp} {Δ : LCtx} {Γ : UCtx} -> h ∈∈ Γ -> h ∈∈ (Δ :: Γ)``

Okay, now we can start the fun stuff. First we define patterns:
``  module Patterns where    open Contexts public       [_] : {A : Set} -> A -> List A    [_] x  = x :: []    -- Pat⁺ Δ A⁺ = linear entailment "Δ ⇒ A⁺"    data Pat⁺ : LCtx -> Pos -> Set where      Px  : {x : Atom} -> Pat⁺ [ HP x ] (X⁺ x)      Pu  : {A⁻ : Neg} -> Pat⁺ [ HN A⁻ ] (↓ A⁻)      P<> : Pat⁺ [] 1⁺      Ppair : {Δ1 : LCtx} { Δ2 : LCtx } {A : Pos} {B : Pos}                -> Pat⁺ Δ1 A -> Pat⁺ Δ2 B -> Pat⁺ (Δ1 ++ Δ2) (A * B)                      Pinl : {Δ : LCtx} {A B : Pos} -> Pat⁺ Δ A -> Pat⁺ Δ (A + B)      Pinr : {Δ : LCtx} {A B : Pos} -> Pat⁺ Δ B -> Pat⁺ Δ (A + B)      Ptt  : Pat⁺ [] 2⁺      Pff  : Pat⁺ [] 2⁺      Pz   : Pat⁺ [] ℕ      Ps   : {Δ : LCtx } -> Pat⁺ Δ ℕ -> Pat⁺ Δ ℕ    -- Pat⁻ Δ A⁻ c = linear entailment "Δ ; A⁻ ⇒ c"    data Pat⁻ : LCtx -> Neg -> Conc -> Set where      Dx  : forall {x} -> Pat⁻ [] (X- x) (CN x)      Dp  : forall {A⁺} -> Pat⁻ [] (↑ A⁺) (CP A⁺)      Dapp : {Δ1 : LCtx } {Δ2 : LCtx} {A⁺ : Pos} {B⁻ : Neg} {c : Conc}               -> Pat⁺ Δ1 A⁺ -> Pat⁻ Δ2 B⁻ c -> Pat⁻ (Δ2 ++ Δ1) (A⁺ → B⁻) c      Dfst   : {Δ : LCtx} {A⁻ : Neg} {B⁻ : Neg} {c : Conc}                -> Pat⁻ Δ A⁻ c -> Pat⁻ Δ (A⁻ & B⁻) c      Dsnd   : {Δ : LCtx} {A⁻ : Neg} {B⁻ : Neg} {c : Conc}                -> Pat⁻ Δ B⁻ c -> Pat⁻ Δ (A⁻ & B⁻) c``

Observe that the constructors for Pat⁺ are just value patterns. The constructors for Pat⁻ are somewhat less familiar: they correspond to patterns for elimination contexts, which are sometimes called spines.

Finally, we define the generic focused sequent calculus:

``  module Logic where    open Patterns public    mutual       -- RFoc Γ A⁺ = right-focus "Γ ⊢ [A⁺]"       data RFoc : UCtx -> Pos -> Set where         Val : forall {Γ A⁺ Δ} -> Pat⁺ Δ A⁺ -> SatCtx Γ Δ -> RFoc Γ A⁺        -- LInv Γ c₀ c = left-inversion "Γ ; c₀ ⊢ c"       data LInv : UCtx -> Conc -> Conc -> Set where         Id- : forall {Γ X- } -> LInv Γ (CN X-) (CN X-)         Fn   : forall {Γ A⁺ c}                 -> ({Δ : LCtx} -> Pat⁺ Δ A⁺ -> UnFoc (Δ :: Γ) c)                 -> LInv Γ (CP A⁺) c       -- RInv Γ h = right-inversion "Γ ⊢ h;"       data RInv : UCtx -> Hyp -> Set where         Susp : forall {Γ A⁻ }                -> ({Δ : LCtx} {c : Conc} -> Pat⁻ Δ A⁻ c -> UnFoc (Δ :: Γ) c)                -> RInv Γ (HN A⁻)         Id+ : forall {Γ X⁺ } -> ((HP X⁺) ∈∈ Γ) -> RInv Γ (HP X⁺)           -- LFoc Γ A⁻ c = left-focus "Γ ; [A⁻] ⊢ c"       data LFoc : UCtx -> Neg -> Conc -> Set where         Spine : forall {Δ A⁻ c0 c Γ} -> Pat⁻ Δ A⁻ c0  ->  SatCtx Γ Δ  ->  LInv Γ c0 c                 -> LFoc Γ A⁻ c       -- UnFoc Γ c = unfocused "Γ ⊢ c"       data UnFoc : UCtx -> Conc -> Set where         Ret : forall {Γ A⁺ } -> RFoc Γ A⁺ -> UnFoc Γ (CP A⁺)         App : forall {Γ A⁻ c} -> ((HN A⁻) ∈∈ Γ) -> LFoc Γ A⁻ c -> UnFoc Γ c       -- SatCtx Γ Δ = conjoined inversion "Γ ⊢ Δ;"       data SatCtx : UCtx -> LCtx -> Set where         Sub : forall {Γ Δ} ->               ({h : Hyp} -> (h ∈ Δ) -> (RInv Γ h))               -> SatCtx Γ Δ``

Some examples follow (translated from this paper). Here's where Agda's second most important feature (after Unicode support) gets to show off: dependent pattern-matching! We reuse Agda's coverage checker to ensure that our object-level functions are total.
``  module Examples where    open Logic    NilCtx : {Γ : UCtx} -> SatCtx Γ []    NilCtx = Sub f     where f : forall {h} -> h ∈ [] -> RInv _ h           f ()    ⌊_⌋ : {Δ : LCtx} -> Pat+ Δ 2⁺ -> Pat+ [] 2⁺    ⌊_⌋ Ptt = Ptt    ⌊_⌋ Pff = Pff    tt : {Γ : UCtx} -> RFoc Γ 2⁺    tt = Val Ptt NilCtx    ff : {Γ : UCtx} -> RFoc Γ 2⁺    ff = Val Pff NilCtx    not : (Γ : UCtx) -> RInv Γ (HN (2⁺ → ↑ 2⁺))    not Γ = Susp not*      where        not* : {Δ : LCtx} {c : Conc} -> Pat- Δ (2⁺ → ↑ 2⁺) c -> UnFoc (Δ :: Γ) c        not* (Dapp Ptt Dp) = Ret ff        not* (Dapp Pff Dp) = Ret tt    and : (Γ : UCtx) -> RInv Γ (HN (2⁺ → 2⁺ → ↑ 2⁺))    and Γ = Susp and*      where        and* : {Δ : LCtx} {c : Conc} -> Pat- Δ (2⁺ → 2⁺ → ↑ 2⁺) c -> UnFoc (Δ :: Γ) c        and* (Dapp Ptt (Dapp Ptt Dp)) = Ret tt        and* (Dapp Ptt (Dapp Pff Dp)) = Ret ff        and* (Dapp Pff (Dapp Ptt Dp)) = Ret ff        and* (Dapp Pff (Dapp Pff Dp)) = Ret ff    App' : {Γ : UCtx} {A+ B+ : Pos} {c : Conc} ->            (HN (A+ → ↑ B+) ∈∈ Γ) -> (RFoc Γ A+) -> (LInv Γ (CP B+) c) ->           UnFoc Γ c    App' u (Val p σ) F = App u (Spine (Dapp p Dp) σ F)    table1 : (Γ : UCtx) -> RInv Γ (HN (↓(2⁺ → ↑ 2⁺) → ↑ (2⁺ * 2⁺)))    table1 Γ = Susp table1*      where        table1* : {Δ : LCtx} {c : Conc} -> Pat- Δ (↓(2⁺ → ↑ 2⁺) → ↑ (2⁺ * 2⁺)) c -> UnFoc (Δ :: Γ) c        table1* (Dapp Pu Dp) = App' (s0 f0) tt (Fn (\b1 ->                                App' (sS (s0 f0)) ff (Fn (\b2 ->                                      Ret (Val (Ppair ⌊ b1 ⌋ ⌊ b2 ⌋) NilCtx)))))``

## Monday, January 14, 2008

### Back from POPL, forward to AGDA

I arrived back in Pittsburgh yesterday after a week at POPL and related workshops in San Francisco. Modulo the stress of having to prepare my presentation for the last day, it was a lot of fun! Heard lots of interesting talks, and had many interesting conversations. The highlight was probably Conor McBride's performance of "Clowns to the left of me, jokers to the right" ("I watch Olivier Danvy as he circles the room with a knife, threatening to defunctionalize my continuation"), but I also really enjoyed Janis Voigtlaender's talk, "Much Ado about Two". Knuth's 0-1 principle states that any oblivious sorting algorithm can be verified correct simply by testing it on arrays of 0s and 1s. Voigtlaender proved an analogous result for parallel prefix sort: correctness can be verified simply by testing arrays of 0s, 1s, and 2s. The neat thing is that the result can be obtained almost as a "free theorem", i.e. by proving a few simple combinatorial properties and applying parametricity. This paper also seems to me in a similar spirit as Martín Escardó's seemingly impossible functional programs and Kevin Watkin's 98-line proof of Conway's Cosmological Theorem─very clever uses of Haskell to reduce a seemingly infinite search space to a finite one. These sort of results make me feel optimisic about the future.

Another thing that makes me feel optimistic: Agda2. Dan Licata and I had a coding session today to try to translate focusing-with-higher-order-rules into Agda, and it seems almost perfectly suited. Dependent pattern-matching and unicode: a killer combination. I will try to post more about this in the next few days.