The Paralyzing Paradoxes of Professor Polaro

reflecting and reifying the state monad

2010-09-29T07:26:00.000-07:00

The Haskell code below was inspired by Andrej Bauer's visit last week, as well as thinking more about this, this, and this since writing this.


{-# LANGUAGE RankNTypes, FlexibleInstances #-}

-- A "negative type" is a datatype of continuations, indexed by answer
-- type.  Given such a description, we can define values, "algebras",
-- and "handlers" as control expressions ("double negations") with
-- different answer type constraints
-- (cf. http://polaro.blogspot.com/2010/05/five-kinds-of-double-negation.html)

newtype Value neg = Val { runVal :: forall r. neg r -> r }
newtype Algebra neg r = Alg { runAlg :: neg r -> r }
newtype Handler neg r1 r2 = Han { runHandle :: neg r1 -> r2 }

infixr 0 `plugV`, `plugA`, `plugH`

plugV :: neg r -> Value neg -> r
k `plugV` v = runVal v k

plugA :: neg r -> Algebra neg r -> r
k `plugA` v = runAlg v k

plugH :: neg r -> Handler neg r r' -> r'
k `plugH` v = runHandle v k

-- We define the negative type Cell s

data Cell s r = Update s (Cell s r)
              | Lookup (s -> Cell s r)
              | Return r

-- Example: given an initial state, we can create a cell value...

new :: s -> Value (Cell s)
new s = Val newVal
    where
      newVal (Update s' k) = k `plugV` new s'
      newVal (Lookup ks) = ks s `plugV` new s
      newVal (Return a) = a

-- Example: perform some operations on an initial state...

r1 = (Lookup $ \s ->
      Update (s-1) $
      Lookup $ \s' ->
      Return (s'+1))
     `plugV`
     new 2
-- r1 = 2

-- Monadic reification and reflection

reify :: Cell s a -> s -> (s,a)
reify k s = k `plugH` Han reifyHandle
    where
      reifyHandle (Update s' k') = reify k' s'
      reifyHandle (Lookup ks) = reify (ks s) s
      reifyHandle (Return a) = (s,a)

reflect :: (s -> (s,a)) -> Cell s a
reflect m = Lookup $ \s ->
            let (s',a) = m s in
            Update s' $
            Return a

-- Example: Normalization by reification and reflection

prog1 = Update 0 $
        Lookup $ \s ->
        Return (s + 1)
prog2 = Lookup $ \s ->
        Update 2 $
        Update 0 $
        Return 1

-- a bit of code for printing cell continuations (prints only a small
-- segment of lookup tables)
instance Show r => Show (Cell Integer r) where
    show (Update s k) = "upd " ++ show s ++ "; " ++ show k
    show (Lookup ks) = show (map (\s -> (s, ks s)) [0..3])
    show (Return a) = "ret " ++ show a

-- *Main> prog1
-- upd 0; [(0,ret 1),(1,ret 2),(2,ret 3),(3,ret 4)]
-- *Main> prog2
-- [(0,upd 2; upd 0; ret 1),(1,upd 2; upd 0; ret 1),(2,upd 2; upd 0; ret 1),(3,upd 2; upd 0; ret 1)]
-- *Main> reflect(reify prog1)
-- [(0,upd 0; ret 1),(1,upd 0; ret 1),(2,upd 0; ret 1),(3,upd 0; ret 1)]
-- *Main> reflect(reify prog2)
-- [(0,upd 0; ret 1),(1,upd 0; ret 1),(2,upd 0; ret 1),(3,upd 0; ret 1)]

Otherwise, things have been good. This blog has been quiet for a while, but I'm still learning a lot from amazing people. Though I can't resist quoting Henry Miller: "It is now the fall of my second year in Paris. I was sent here for a reason I have not yet been able to fathom."

Five kinds of double-negation

2010-05-22T11:06:00.000-07:00

A recent question on the TYPES mailing list reminded me that one reason negation is confusing is because it can mean so many different things. I and others originally thought the answer the person was looking for (the type-theoretic reading of negation) was "continuations", but it turned out his intuition was about a different form of negation not usually considered in constructive logic (but available in "refinement type systems", etc.), since it's tied to the "extrinsic" interpretation of types-as-properties. (For more on this deficit of constructive logic, see the introduction to Paul Taylor's Subspaces in Abstract Stone Duality.)

But even restricted to plain old type theory, there are many different interpretations of negation! Under the principle of "Why talk about something confusing when you can talk about something doubly confusing?", today I want to talk about different computational interpretations of double negations in logic.

(A -> 0) -> 0. Here 0 is falsehood, and this is the standard interpretation of double-negation in intuitionistic logic. What does this mean computationally? Well, one way to think about this is to interpret types as sets. How many different functions f : X -> 0 are there from any set X into the empty set? None, unless X is itself empty, in which case there is exactly one. Applying this reasoning to our double-negation, if A is non-empty, then A -> 0 is empty, which in turn means that (A -> 0) -> 0 contains exactly one element; conversely, if A is empty, then A -> 0 is non-empty, which in turns means that (A -> 0) -> 0 is empty. What we see is that intuitionistic double-negation encodes the principle of proof-irrelevance, i.e., it forgets all the computational content of a type. (The catch here is that set-theoretic reasoning doesn't always prove type isomorphisms—this argument really only works for extensional type theory.)
(A -> ⊥) -> ⊥. Here ⊥ represents "minimal" falsehood, i.e., simply a logical atom with no introduction or elimination rules, and in particular without the principle of explosion. Because we have replaced "empty" with "unknown", minimal double-negation does not have the same computational degeneracy of intuitionistic double-negation: there are at least as many different constructive proofs of (A -> ⊥) -> ⊥ as there are of A, and often more. For example, in general there is no proof in minimal logic of excluded middle A ∨ (A -> ⊥), but there is a proof of ((A ∨ (A -> ⊥)) -> ⊥) -> ⊥. Indeed, minimal logic rather than intuitionistic logic really is the proper place to understand the computational content of the classical double-negation translations (something which I didn't fully appreciate until reading Jeremy Avigad's The computational content of classical arithmetic). As such, this form of double-negation is the first step towards understanding continuation-passing style.
(A -> R) -> R, where R is any type of answers. We said that ⊥ above is a logical atom. In type-theoretic terms, it is a type variable. So to move to this form double-negation, we simply instantiate the variable with a concrete type R. Now, logically we are beginning to stretch the meaning of "negation". In particular, nothing says that R is uninhabited—indeed if it is provably uninhabited, we are back to the computationally degenerate situation (1). But whether or not we accept the terminology, this form of double-negation is extremely important computationally, tied to the representation of control flow. A function of type A -> R is a continuation (transforming any value of type A into a result of type R), and so a term of type (A -> R) -> R is something which takes a continuation to a result—a computation with "control effects". The type (A -> R) -> R is so powerful that it comes with the following warning:Abuse of the Continuation monad can produce code that is impossible to understand and maintain.The "principle of double-confusion" I mentioned at the beginning then motivates the following pair of generalizations...
(A -> R1) -> R2, where R1 and R2 are two (possibly distinct) types of answers. This form of double-negation comes up in the study of delimited control operators, which were originally motivated by the fact that the type (A -> R) -> R is not only too powerful but also not powerful enough. The type (A -> R1) -> R2 can be seen as a sort of Hoare triple {R1}A{R2}, which gives an intimation of its power.
∀α.(A -> α) -> α, a polymorphic type (and more generally, ∀α.(A -> Tα) -> Tα, where T is an arbitrary monad). It's easy to see that A ≡ ∀α.(A -> α) -> α is provable in second-order intuitionistic logic, but in fact this can also be interpreted as the Yoneda isomorphism in category theory, as sigfpe explained a few years ago. More generally, there is a Yoneda isomorphism between TA and ∀α.(A -> Tα) -> Tα for any monad T (and formally, a type isomorphism in System F + parametricity axioms). This isomorphism lies at the heart of Filinski's representation theorem that delimited control operators can be used to perform "monadic reflection".

So that is a small cast of characters, biased towards the view of "negation as continuation" (which as I said, is not the only view). For more plots involving these different forms of double-negation (particularly (4) and (5)), you can read the paper I posted two weeks ago.

Polarity and the logic of delimited continuations

2010-05-02T12:31:00.000-07:00

Text: pdf
Code: twelf
Abstract:

Polarized logic is the logic of values and continuations, and their interaction through continuation-passing style. The main limitations of this logic are the limitations of CPS: that continuations cannot be composed, and that programs are fully sequentialized. Delimited control operators were invented in response to the limitations of classical continuation-passing. That suggests the question: what is the logic of delimited continuations?
We offer a simple account of delimited control, through a natural generalization of the classical notion of polarity. This amounts to breaking the perfect symmetry between positive and negative polarity in the following way: answer types are positive. Despite this asymmetry, we retain all of the classical polarized connectives, and can explain "intuitionistic polarity" (e.g., in systems like CBPV) as a restriction on the use of connectives, i.e., as a logical fragment. Our analysis complements and generalizes existing accounts of delimited control operators, while giving us a rich logical language through which to understand the interaction of control with monadic effects.

To appear at LICS 2010.

Writing this paper helped me sort out some things I'd been puzzled about for a while—I hope you also find it useful!

"One of the first things to learn about category theory is that not everything in mathematics is a category"

2010-04-24T14:12:00.000-07:00

Sorry, apologies, etc., for the long silence. I've been working on the final version of a paper that I plan to post here in a few days. This mini-post is just to highlight an exchange on MathOverflow that jibes with some things I've been thinking about lately. The quote in the title is from Mike Shulman in response to this question, "Why haven’t certain well-researched classes of mathematical object been framed by category theory?" I also like Reid Barton's response, in particular, "From the standpoint of higher category theory, categories (i.e., 1-categories) are just one level among many in a family of mathematical structures". This seems to me like an important lesson to keep in mind when applying category theory to programming languages and proof theory: to resist the desire to phrase everything as a category.

Twelf, my favorite general-purpose functional programming language

2010-01-26T15:32:00.000-08:00

(Disclaimer: the title of this post is tongue-in-cheek—I do not really like to play favorites. But hopefully you will understand why I chose it: to mess with your head.)

Last week I was at POPL 2010 in Madrid. Most fun of course was catching up with friends and meeting new people, but there were also some excellent talks. A few highlights:

Swarat Chaudhuri's talk about Continuity Analysis of Programs: continuity, like type safety, provides a measure of the "robustness" of programs
Trevor Jim's very fun talk on Yakker (Semantics and Algorithms for Data-dependent Grammars)
Andrzej Filinski on Monads in Action: exploring the relationship between monadic and operational semantics
Matthias Felleisen's invited talk at TLDI, which opened with the following slide:

In this post I want to talk a bit about my favorite general-purposefunctional programming language, Twelf. If that sentence gives youcognitive dissonance, please read on!

Really, what I am going to be describing is a very shallowembedding of a pure functional language within Twelf. Forfamiliarity (though at a cost of expressiveness), I will limit our language to an ML-like, call-by-valuefragment (with arbitrary recursive datatypes and recursivefunctions), rather than a fully polarized type theory. For fun, ourlanguage will also include Haskell-style typeclasses. Our two weapons will betraditional LF-style (dependently-typed) higher-order abstract syntax, and thedefunctionalization trick I described a year ago. Don't worry, we won't be proving any theorems, only writing programs.

We begin by declaring the (meta-level) type of (object-level) types:


tp : type.                      % types

As we did informally in a previous post, we will distinguish three syntactic categories:


val : tp -> type.               % values
kon : tp -> tp -> type.         % "delimited" continuations
exp : tp -> type.               % expressions

(Note: there is nothing scary about delimited continuations—think of them as pure ML functions, or entailments, or morphisms in a category.) Expressions in our language are constructed out of values and continuations, as follows:


! : val A -> exp A.             %prefix 10 !.
$ : kon A B -> exp A -> exp B.  %infix right 11 $.

Because we are really restricting to types of positivepolarity, values are built by applying constructors, whilecontinuations are defined by pattern-matching on values. Thelatter principle is expressed (in defunctionalized form) by the apply function, a Twelf logic program:


apply : kon A B -> val A -> exp B -> type.
%mode apply +K +V -E.

Now, without knowing anything else about values and continuations,we can already give our language a generic (big-step) operationalsemantics:


eval : exp A -> val A -> type.
%mode eval +E -V.
- : eval (! V) V.
- : eval (F $ E) VR
        <- eval E V
        <- apply F V E'
        <- eval E' VR.

And that's the core language! Next we can build up a nice libraryof datatypes and library routines. We define some simple datatype constructors, by their value constructors:


1 : tp.
<> : val 1.

0 : tp.

* : tp -> tp -> tp.             %infix right 12 *.
pair : val A -> val B -> val (A * B).

+ : tp -> tp -> tp.             %infix right 11 +.
inl : val A -> val (A + B).
inr : val B -> val (A + B).

=> : tp -> tp -> tp.            %infix right 10 =>.
fn : kon A B -> val (A => B).

We also introduce polymorphic and recursive types (noteour reliance on HOAS and substitution):


∀ : (tp -> tp) -> tp.
Λ : ({x}val (A x)) -> val (∀ A).

rec : (tp -> tp) -> tp.
fold : val (A* (rec A*)) -> val (rec A*).

Finally we derive some familiar datatypes:


bool = 1 + 1.
true = inl <>.
false = inr <>.

maybe = [A] A + 1.
nothing : val (maybe A) = inr <>.
just : val A -> val (maybe A) = [V] inl V.

nat = rec [X] 1 + X.
z : val nat = fold (inl <>).
s : val nat -> val nat = [V] fold (inr V).

list = [A] rec [X] 1 + A * X.
nil : val (list A) = fold (inl <>).
cons : val A -> val (list A) -> val (list A) =
        [V] [Vs] fold (inr (pair V Vs)).

Just as we do in Haskell, we can define continuations (functions)by giving them a type declaration, and then a list of pattern-matching clauses. For example, here we define theboolean operations "and" and "or":


and : kon (bool * bool) bool.
- : apply and (pair true true) (! true).
- : apply and (pair true false) (! false).
- : apply and (pair false _) (! false).

or : kon (bool * bool) bool.
- : apply or (pair false false) (! false).
- : apply or (pair false true) (! true).
- : apply or (pair true _) (! true).

We can also define some continuation constructors in the same way.For example, we can define the beloved lambda:


λ : (val A -> exp B) -> kon A B.
- : apply (λ F) V (F V).

λ constructs a continuation from an expression with a free valuevariable, which is useful when we don't need to pattern-matchon the argument. We also define some useful syntactic sugar:


let : exp A -> (val A -> exp B) -> exp B = [E] [F] λ F $ E.

In effect here we are using Twelf as a macrosystem for our embedded language. The following continuationconstructors correspond to (sequent calculus) "left rules" forthe various type constructors:


split : (val A -> val B -> exp C) -> kon (A * B) C.
- : apply (split E*) (pair V1 V2) (E* V1 V2).

case : kon A C -> kon B C -> kon (A + B) C.
- : apply (case K1 K2) (inl V) E
        <- apply K1 V E.
- : apply (case K1 K2) (inr V) E
        <- apply K2 V E.

funsplit : (kon A B -> exp C) -> kon (A => B) C.
- : apply (funsplit E*) (fn F) (E* F).

gensplit : (({x}val (A x)) -> exp C) -> kon (∀ A) C.
- : apply (gensplit E*) (Λ V) (E* V).

unfold : kon (A* (rec A*)) C -> kon (rec A*) C.
- : apply (unfold K) (fold V) E
        <- apply K V E.

Note we are not obligated to use these constructors to definecontinuations, i.e., they are not part of the language specification:they are just library routines. Here's an example of a recursivedefinition:


append : kon (list A * list A) (list A).
- : apply append (pair nil L2) (! L2).
- : apply append (pair (cons V L1) L2)
     (let (append $ ! pair L1 L2) [L'] ! cons V L').

Okay, hopefully by now you are convinced that in this style we we canwrite more or less ordinary (effect-free) ML programs. Next we turnto typeclasses. Typeclasses are basically type-indexed (or typeconstructor-indexed) records, and so their encoding in Twelf followsthe same pattern of defunctionalization (i.e., for thepolarity-sensitive, because they are negative values).Here we introduce a few typeclasses familiar from Haskell:


EQ : tp -> type.
eq : EQ A -> kon (A * A) bool.

FUNCTOR : (tp -> tp) -> type.
fmap : FUNCTOR F -> kon A B -> kon (F A) (F B).

MONAD : (tp -> tp) -> type.
eta : MONAD T -> kon A (T A).
ext : MONAD T -> kon A (T B) -> kon (T A) (T B).

% Wadler's syntactic sugar...
return : MONAD T -> exp A -> exp (T A) = [M] [E] eta M $ E.
bind : MONAD T -> exp (T A) -> kon A (T B) -> exp (T B) = [M] [E] [K] ext M K $ E.

We can instantiate EQ in various ways:


1eq : EQ 1.
- : apply (eq 1eq) (pair <> <>) (! true).

sumeq : EQ A -> EQ B -> EQ (A + B).
- : apply (eq (sumeq EqA EqB)) (pair (inl Va1) (inl Va2))
        (eq EqA $ ! pair Va1 Va2).
- : apply (eq (sumeq EqA EqB)) (pair (inl Va1) (inr Vb2))
        (! false).
- : apply (eq (sumeq EqA EqB)) (pair (inr Vb1) (inl Va2))
        (! false).
- : apply (eq (sumeq EqA EqB)) (pair (inr Vb1) (inr Vb2))
        (eq EqB $ ! pair Vb1 Vb2).

paireq : EQ A -> EQ B -> EQ (A * B).
- : apply (eq (paireq EqA EqB)) (pair (pair Va1 Vb1) (pair Va2 Vb2))
       (let (eq EqA $ ! pair Va1 Va2) [x]
          let (eq EqB $ ! pair Vb1 Vb2) [y]
          and $ ! pair x y).

nateq : EQ nat.
- : apply (eq nateq) (pair z z) (! true).
- : apply (eq nateq) (pair z (s _)) (! false).
- : apply (eq nateq) (pair (s _) z) (! false).
- : apply (eq nateq) (pair (s N1) (s N2)) (eq nateq $ ! pair N1 N2).

Likewise FUNCTOR:


idf : FUNCTOR ([A]A).
- : apply (fmap idf K) V E
     <- apply K V E.

prodf : FUNCTOR F -> FUNCTOR G -> FUNCTOR ([A] F A * G A).
- : apply (fmap (prodf F G) K) (pair V1 V2)
     (let (fmap F K $ ! V1) [x] let (fmap G K $ ! V2) [y] ! pair x y).

expf : FUNCTOR ([A]B => A).
- : apply (fmap expf K) (fn K') (! fn (λ [x] K $ K' $ ! x)).

listf : FUNCTOR ([A]list A).
- : apply (fmap listf K) nil (! nil).
- : apply (fmap listf K) (cons V VS) (let (K $ ! V) [x]
                                  let (fmap listf K $ ! VS) [xs]
                                  ! cons x xs).

And MONAD:


idm : MONAD ([a]a).
- : apply (eta idm) V (! V).
- : apply (ext idm K) V E
     <- apply K V E.

maybem : MONAD ([a]maybe a).
- : apply (eta maybem) V (! just V).
- : apply (ext maybem K) V (case K (λ [_] ! nothing) $ ! V).

And now an example where we run fmap on a pair of lists, usingTwelf's logic engine to automatically infer the appropriateinstance of FUNCTOR:


%query 1 *
  eval (fmap F (λ [x] ! s x) $
            ! pair (cons z (cons z nil)) (cons (s z) (cons (s z) nil))) R.
---------- Solution 1 ----------
R = pair (cons (s z) (cons (s z) nil)) (cons (s (s z)) (cons (s (s z)) nil));
F = prodf listf listf.
____________________________________________

And finally, a slightly more involved example:


cond : exp C -> exp C -> kon bool C =
    [E1] [E2] case (λ [_] E1) (λ [_] E2).

lookup : EQ A -> val A -> kon (list (A * B)) (maybe B).
- : apply (lookup Eq V) nil (! nothing).
- : apply (lookup Eq V) (cons (pair V' VE) Vs)
     (cond (lookup Eq V $ ! Vs) (! just VE) $ 
        (eq Eq $ ! pair V V')).

one = s z. two = s one. three = s two. four = s three.
%query 1 *
  eval (bind _ (lookup _ one $ ! cons (pair z three)
                  (cons (pair one four) (cons (pair two z) nil)))
          (λ [x] return _ (! s x))) R.
---------- Solution 1 ----------
R = just (s four).
____________________________________________

And that's the gist of it.

If you are still reading this, perhaps you will be inspired and useour favorite general-purpose functional programming language to write,say, a webserver?

The History of Categorical Logic

2009-12-21T16:02:00.000-08:00

I'm currently making my way through Jean-Pierre Marquis and Gonzalo E. Reyes' 116-page-long The History of Categorical Logic, and it is fascinating. Someone needs to make it into a comic book. [HT: This Week's Finds]

What is the logic of ML values?

2009-11-16T17:10:00.000-08:00

Before approaching the question, "What is the logic of ML values?", Ifirst want to explain why there is more subtlety to the question thanis often assumed.

(Warning: this is a long post on something which most people probablycare very little about. On the other hand, there are 19 google hits for"logic changed my life".)

In general, how does one interpret the question, "What is the logic ofX?", for some programming language X? A standard response is that thelogical theorems are exactly the inhabited types, i.e., types τ suchthat there is a closed term t:τ. But what are the "terms"? Theanswer is obvious enough in simple formal systems where there is onlyone typing judgment, and so we can say things like, "The inhabitedtypes of simply-typed lambda calculus are exactly the theorems ofminimal implicational logic". Yet, real programming languages usuallyhave many different typing judgments, since programs are composed outof many different syntactic objects. In ML, in particular, a programincludes some let-bound values and expressions, some functiondefinitions, and a result expression (in addition to datatypedefinitions, module definitions, etc., which are classified bydifferent kinds of "types").

(In this post, "ML" is meant in a slightly fuzzy but essentiallyunambiguous way, as a call-by-value language with effects. To settlea concrete interpretation, I will be giving examples in Standard ML of NJ, which notablyprovides the control operator callcc. "Value" is meant in thestandard operational sense, i.e., a value is a fully evaluated MLexpression. We can similarly ask, "What is the logic of Haskellvalues?", but that is a different, trickier question, to which I'mstill not sure of the answer.)

When answering the question, "What is the logic of ML?" (or "What isthe logic of Haskell?"), the standard approach is to gloss over thesedifferent syntactic categories, and assume we are talking aboutexpressions. This makes some sense, insofar as this is the largestsyntactic category: all values and functions are also expressions.And expressions also have easy-to-understand principles ofcomposition. For example, the rule of application—from twoexpressions e₁:σ→τ and e₂:σ, we can form the expression (e₁ e₂):τ—witnesses the logical principle of modus ponens. Whereas fromtwo values v₁:σ→τ and v₂:σ, the application (v₁ v₂):τ is nolonger a value.

Yet, I believe it is a mistake to define "the" logic of a programminglanguage in this way, without realizing there is finer structure.That is why I phrased the question, "What is the logic of MLvalues?", rather than full-stop, "What is the logic of ML?"And so how does the logic of ML values differ from the logic of MLexpressions?

Well, it is often claimed that ML (and likewise Haskell) defines aninconsistent logic. This is a statement about the logic of expressions.For example, non-terminating expressions such as

fun loop() = loop()

inhabit every type, as do exception-raising expressions, such as

fun fail() = raise (Fail "inconsistent!?")

(Note: the expressions here are loop() andfail(). Here and below, I assign names toexpressions by declaring them as thunks.)But none of these are values. Indeed, evaluation of the firstexpression will never yield a result,

- loop();
(* waiting a long time... *)

whereas the second will return immediately, but with an exception rather than a value:

- fail();
uncaught exception Fail [Fail: inconsistent!?]
raised at: stdIn:2.3-3.5

(There are some additional complaints about the value restrictionwhen evaluating these polymorphic expressions, but for ourpurposes we can ignore them here.)In fact, the logic of ML values is consistent, as we can see bydefining the empty type:

data void = Void of void

There are no values of type void, since the only way to construct oneis by already having one. Note, though, that all bets are off "undera lambda"—we can still build a value inhabiting any function typeσ→τ, for example

fun fnfail() = fn _ => raise (Fail "inconsistent!?")

Let's try to be a bit more precise about what happens before we reachthat point.

Another folk theorem about "the logic of ML" is that insofar as it isconsistent (i.e., if you avoid things like unrestricted recursion andexceptions), with the addition of control operators it becomesclassical. We can import the relevant SML/NJ library andsee what they mean:

- open SMLofNJ.Cont;
opening SMLofNJ.Cont
type 'a cont = 'a ?.cont
val callcc : ('a cont -> 'a) -> 'a
val throw : 'a cont -> 'a -> 'b
val isolate : ('a -> unit) -> 'a cont
(* ... *)

As first observed by Griffin, the type of callcc correspondslogically to the classical principle of Peirce's Law. We canmake this a bit easier to see by defining another controloperator letcc, which essentially does the samething as callcc but with first-class ML functions, rather thanvalues of the cont type:

- fun letcc f = callcc (fn k => f (fn x => throw k x));
val letcc = fn : (('a -> 'b) -> 'a) -> 'a

Using letcc, we can derive the law of excluded middle, ∀α.α ∨ ¬α.To represent this type, we first introduce a type constructorfor disjunctions:

data ('a,'b) either = Left of 'a | Right of 'b

Now we can witness excluded middle as follows:

fun excluded_middle() : ('a,'a -> void) either =
letcc (fn k => Right (fn x => k (Left x)))

So what happens when we attempt to evaluate this expression? (To avoid complaints about the value restriction, we instantiate the type variable 'a at some arbitrary type a.)

- excluded_middle() : (a,a -> void) either;
val it = Right fn : (a,a -> void) either

And now, in contrast to what happened above with the evaluation ofloop() and fail(), here we actually get a value!

So can we say that the logic of ML values really is classical?Well, we evidently can under the "bag of tautologies" view of logic.But that is not necessarily the most useful view.

If we look up at the above ML session, a shockingly anti-classicalprinciple is already staring back down at us. After evaluatingexcluded_middle(), we got back this value:

val it = Right fn : (a,a -> void) either

That is, not only is this a proof of α ∨ ¬α, but in fact it containsa proof of the right side of the disjunct, ¬α. This is an instance of the intuitionistic disjunctionprinciple, that a proof of a disjunction is a proof of one of thetwo disjuncts.

The punchline, I would say, is that the logic of ML values isnot unsound, and not classical, but simply constructive.What is an ML value of type τ? Just an intuitionistic proofof τ—but in a non-empty context. This context includes the currentcontinuation of type ¬τ, as well as all of the other effects that canbe invoked underneath a lambda, i.e., in values of functionaltype.

Okay, so what have we brushed over here? Well first, the restrictionthat effects are only invoked underneath lambdas can actually beenforced by CPS translation. Functions σ→τ are interpreted as¬(σ∧¬τ), where ¬(-) denotes minimal negation, i.e., ¬τ = τ→β, for somefixed parameter β, the return type. Effectful operations areencoded as things that return β. Second, I said that a value of (aCPS translated) type τ is an intuitionistic proof of τ (in a non-emptycontext of effects), but are all such intuitionstic proofsvalues? Well, no, because some proofs involve "detours". To beconcrete, if M₁ and M₂ are proofs of σ and τ, then π₁(M₁, M₂) is aproof of σ—yet, #1 ("hello", "world") is typically notconsidered to be a value (it evaluates to "hello"). (Somepeople like to call expressions like #1 ("hello","world") "valuable".) Third, to say that there is a "logic" ofML values, we really do have to explain what its compositionprinciples are, and not just which principles fail. I might revisitsome of these points in another post.

Finally, the whole idea of a "logic of ML values" is very close to theidea of the realizability interpretation of ML. Some people believe thatrealizability is a distinct and very different alternative to Curry-Howard as aconstructive interpretation of logic. My point with this post was mainlyto suggest that Curry-Howard need not exclude realizability-likeinterpretations, once we realize (so to speak) that there is more than one syntacticcategory of proofs.

Big-Step Normalisation

2009-10-28T04:03:00.000-07:00

I realized that the idea of the previous post of factoring normalization as a translation to and from a syntactic model of normal forms is explored very nicely in a JFP article by Altenkirch and Chapman, indeed with a concrete environment semantics, albeit without a connection to focusing:

"Big-Step Normalisation"
Thorsten Altenkirch and James Chapman
pdf
Abstract:
Traditionally, decidability of conversion for typed λ-calculi is established by showing that small-step reduction is conﬂuent and strongly normalising. Here we investigate an alternative approach employing a recursively defined normalisation function which we show to be terminating and which reﬂects and preserves conversion. We apply our approach to the simply-typed λ-calculus with explicit substitutions and βη-equality, a system which is not strongly normalising. We also show how the construction can be extended to System T with the usual β-rules for the recursion combinator. Our approach is practical, since it does verify an actual implementation of normalisation which, unlike normalisation by evaluation, is ﬁrst order. An important feature of our approach is that we are using logical relations to establish equational soundness (identity of normal forms reﬂects the equational theory), instead of the usual syntactic reasoning using the Church-Rosser property of a term rewriting system.

Normalization-By-Evaluation, Normalization-By-Focusing

2009-10-11T11:56:00.000-07:00

So I've moved to Paris. I finally arrived here last week (after a bit of a summer vacation), to begin a post-doc at Université Paris 7. In addition to my host Paul-André Melliès, there is a ridiculous number of people based here doing exciting work in programming and proof theory, and also quite a few visitors. So I'm excited.

One of my goals with this post-doc is to better connect the general approach to logic and programming that I was trained in at CMU, which could be called a "syntactic" approach, to the more semantic approach prevalent in Europe. "Syntactic" is in scare quotes because it is sometimes used as a derogatory term, slightly gentler than the epithet "symbol-pushing", and I don't think it is really appropriate. Of course I wouldn't think so! But there's a burden of proof in explaining how this thing that looks like symbol-pushing to the outside world is actually just another way (and a useful way) of manipulating semantic content.

So this post is in that vein, and was prompted by hearing Danko Ilik (one of Hugo Herbelin's students) give a talk two days ago about Normalization-By-Evaluation (NBE), and its apparently well-known (but I guess not well-known enough, since I hadn't seen it before) connection to Kripke semantics for intuitionistic logic. The connection is extremely easy to state:

NBE = completeness ○ soundness

That is, constructively speaking, NBE for the lambda calculus (a.k.a. a proof system for intuitionistic logic) corresponds to applying the soundness theorem (if something is provable it is true in every Kripke model) followed by the completeness theorem (if something is true in every Kripke model then it is provable). More precisely, the soundness theorem is applied to bring a lambda term into the universal model of contexts ordered by inclusion, and then the completeness theorem takes it back into the lambda calculus, now in normal form. Darin Morrison recently posted some elegant code to the Agda mailing list, demonstrating this explicitly.

Okay, that's neat, now let's talk about something else: focusing. If you are reading this blog you have probably heard something about it. (If not, you can learn about it here or here or here or here or here or here.) Originally, focusing was conceived as a search strategy for linear logic sequent calculus, achieving efficiency by severely restricting when you could apply the different rules, based on the polarity of connectives (positive ⊗, ⊕, !, ∃, versus negative ⅋, &, ?, ∀). The surprising and important result was that this strategy is complete, i.e.:

THEOREM (Completeness of focusing) [Andreoli]: If the sequent Γ ⊢ Δ is provable in linear logic, then it has a focusing proof.

The converse, soundness, is of course also important, but was obvious in Andreoli's original formulation, where focusing was seen as a search strategy, and a focusing proof was just a special sort of sequent proof.

Nonetheless, we have soundness and completeness theorems. Great! Can we compose them?

Well, let's not go there quite yet...

First, let's move away from linear logic, which may seem exotic, to something more mundane: classical propositional logic. Is there a notion of focusing proofs in classical logic? In fact, there are too many. Whereas the polarities of the connectives of linear logic are all somehow fixed by their inference rules, in classical logic there are many different, equally valid possibilities for inference rules, and as a result the propositional connectives are fundamentally bipolar. The flip side is that the classical connectives can be explicitly polarized, e.g.., we can choose whether to treat conjunction ∧ positively as ⊗, or negatively as &, and similarly with disjunction, negation, and implication. And this act of disambiguation endows the classical connectives with constructive content.

How so?

Well, let's take another look at the soundness and completeness theorems for focusing. Since focusing proofs deal with explicitly polarized propositions, and ordinary (classical) proofs don't, we will relate the two notions via an operation |-| that "forgets" polarity, i.e., collapses ⊗ and & both to plain conjunction, ⅋ and & both to plain disjunction, etc. Then we can state the following:

THEOREM (Classical soundness of focusing): If the sequent Γ ⊢ Δ has a focusing proof, then |Γ| ⊢ |Δ| has an ordinary classical proof.

THEOREM (Classical completeness of focusing): If the sequent |Γ| ⊢ |Δ| has an ordinary classical proof, then Γ ⊢ Δ has focusing proof.

So now can we compose?

Again speaking more constructively, suppose we take as our starting point some version of classical natural deduction, e.g., natural deduction adjoined with reductio ad absurdum, or with Peirce's law, a.k.a. lambda calculus with control operators. And suppose we have a proof (program) establishing (inhabiting) some proposition (type). Now, to apply the completeness theorem to obtain a focusing proof/program, crucially, we must choose some polarization of the connectives. What we obtain by applying the completeness theorem can and will depend on the particular polarization. But then, once we have a focusing derivation, we can again obtain a classical derivation in a deterministic way, by applying the soundness theorem.

And what do we get as a result? Well, we can make two observations:

1. The result is in normal form. I.e., it corresponds to a β-reduced, η-expanded lambda term (or a sequent calculus proof without cuts and with only atomic initial axioms).
2. The result is in continuation-passing style (CPS).

And in fact, the choice we made when applying the completeness theorem—the way we polarized the connectives—is precisely the way we choose among the many different CPS translations, call-by-value vs call-by-name, etc.

[Aside: it is well-known that different CPS transformations correspond to different double-negation translations, proof-theoretically. This may seem at odds with the above statement, since the result of applying completeness followed by soundness is still a proof of the original sequent, not a double-negated sequent. But we can make the connection to double-negation translation more transparent by factoring the soundness theorem by way of minimal logic, i.e, the fragment of intuitionistic logic where negation is defined by ¬A = A ⊃ #, for some distinguished atom #. The soundness theorem is then stated as follows:

THEOREM (Minimal soundness of focusing): If the sequent Γ ⊢ Δ has a focusing proof, then Γ^t, Δ^f ⊢ # has an ordinary minimal proof.

Here, -^t is the operation that interprets positive connectives "directly" (i.e., conjunction as conjunction, disjunction as disjunction, etc.) and interprets negative connectives as the negation of their De Morgan duals, while -^f interprets negative connectives as their duals, and positive connectives as their negations. Now, the result of applying the classical completeness theorem followed by minimal soundness, followed by the inclusion of minimal logic into classical logic, is not necessarily the original sequent, but a (classically) equivalent one. For more details, see Chapters 3 and 4 of my thesis.]

In short, by composing the soundness and completeness theorems for focusing, we obtain a normalization procedure for a proof system/programming language, that moreover fixes an evaluation order based on the polarization. We could call this "Normalization-By-Focusing":

NBF = soundness ○ completeness

So how does this compare to the original equation, NBE = completeness ○ soundness? First, observe that the fact that the positions of soundness and completeness are swapped is purely a historical convention! Since focusing was originally conceived as a search strategy for sequent calculus, it made sense to ask that it be complete. But in any case, it is clear that the focusing completeness theorem is playing a role analogous to the Kripke soundness theorem, and the focusing soundness theorem a role analogous to the Kripke completeness theorem. In other words, in both cases we are going out of a formal system with some arbitrary collection of rules, into a very well-behaved system, and then back into a canonical fragment of the original system.

In other words, I think it is entirely accurate to say that focusing provides a semantics of proofs. And a proof-theoretic semantics at that.

But how does it really relate to other semantic approaches? Again, that's what I'm here to find out. I suspect, though, that there's more than a superficial resemblance between the NBE and NBF equations, and there might be a deeper connection between focusing and the technique of forcing in proof theory.

More on LOGICOMIX, from Richard Zach

2009-09-30T14:31:00.000-07:00

Richard Zach of LogBlog also wrote a review of Logicomix last week, and today followed up specifically addressing the novel's theme of Logic and Madness. This was something I left out of my review, but like Zach, I was similarly turned off by the novel's insinuations of a positive correlation. Both posts by Zach point out several historical inaccuracies in Logicomix, where the novel overstates the "madness" of various logicians—important to keep in mind when reading Logicomix (which you should, nonetheless...).

Review of LOGICOMIX

2009-09-15T15:26:00.000-07:00

I was in New York City yesterday visiting the French consulate, on a mission to obtain a scientific visa (my second attempt). The bus from Rochester got into Chinatown around 7:45am, so I made it to the consulate by 9am, got in line, handed in my documents, had a few pictures/fingerprints taken, and was told to come back at 3pm to pick up a visa. With a few hours to kill in the city, I set out on another mission: to find a copy of Logicomix!

LOGICOMIX: an Epic Search for Truth
Apostolos Doxiadis and Christos H. Papadimitriou
art by Alecos Papadatos and Annie di Donna
http://www.logicomix.com/

First, a note on availability. This book was just released to the public in English, I believe a little over a week ago. The UK edition is currently sold out, and the US edition is only available for pre-order on Amazon. So the odds of my finding a copy were perhaps not so good. On the other hand, New York City has the Strand Bookstore. With a bit of luck and perserverance, I managed to track down their only copy, which they received two [sic!] days ago (they are ordering more). I finished reading it on the train ride back to Rochester.

Second, a disclaimer: I had ridiculously high expectations for this book. It has been at the top of my wishlist for years. Anticipation for Logicomix has been floating around the net since the first half of the decade, based on its basic premise: a comic book about logic and logicians. For example, you can find Philip Wadler drooling about the idea back in the summer of 2005. I don't remember when I first found out about Logicomix, but it was a while before that (looking back at old email archives, it seems to have been May 2004), sometime after I heard about Papadimitriou's first work of fiction, Turing: a novel about computation (which is a very fun book, by the way, basically a sci-fi thriller with some computer science lessons thrown in, and some pretty hot sex scenes).

Given all this anticipation built on the idea of Logicomix, reading the actual Logicomix was bound to be somewhat of a let-down. In a word, I was hoping for something impossibly EPIC. Let me say, though, that I still think Logicomix is a revolutionary book, with a brilliant premise that is very well executed but for a few flaws. The premise is basically this: to convey the drama of the late 19th-/early 20th-century upheavals in mathematics and logic, focusing on the people involved, but also giving a sense of their ideas, and of the passion behind the debate. The driving plot force is the life story of Bertrand Russell, and his (at times fictitious) interactions with some of logic's other major and minor figures.

Logicomix is epic in ambition. In some form or another, the book looks at topics including: Euclid's Elements, Cantor's set theory, Boolean algebra, Leibniz's calculus ratiocinator, the 1900 International Congress of Mathematicians and Hilbert's problems, the Epimenides paradox and Russell's paradox, Frege's Begriffsschrift and the Foundations of Arithmetic, Principia Mathematica, simple and ramified type theory, Wittgenstein's Tractatus and the picture theory of language, the Vienna Circle, logical positivism, and the murder of Moritz Schlick, Godel's first incompleteness theorem, algorithms, atheism, World Wars I and II, pacifism, pedagogy, the connection between logic and madness, Aeschylus, street crime in Athens, and free love. And it tries to examine all this as a graphic novel, taking full advantage of the genre's literary/artistic conventions, such as flashbacks and self-reference. The latter fits in well with the subject matter (e.g., Papadamitriou's character asks in the book, "Suppose now you make a complete catalogue of all books that are *not* self-referential"...), but also, more significantly, gives rise to a parallel story relating the intellectual process of writing the book, showing how Logicomix grew through the authors' own debates and discoveries. Finally, a brief appendix at the end tries to fill in some of the historical/mathematical background for the story with a few traditional but well-written articles.

Now, please stop.

Go find a copy of Logicomix (don't worry, they're out there), and read it! You will enjoy it.

I do think the book has flaws, though. I was hoping for Logicomix to do more, but I think in reality it tries to do too much, leaving too much unresolved. There is no doubt something intentional here on the part of the authors, in reference to their subject matter. A chunk of the story revolves around the arduous task of writing the Principia, and how Whitehead after ten years finally convinces Russell to publish their manuscript, even in its unfinished, very imperfect state. Through the self-referential segments of Logicomix, it is strongly implied that the authors had similar discussions of their own. But of course that's not an excuse! I would have liked to have seen some of the historical characters fleshed out more, and could have used less of the "behind the scenes" with the writers. The latter had the feeling of unedited transcripts—again, this was certainly intentional, but I felt it took away from the intensity of the main story. Similarly, I didn't like the overall framing device of having Bertrand Russell relate his life story at a public lecture on "The Role of Logic in Human Affairs": again, because it dilutes the action through another level of indirection, and also because it is a completely implausible lecture. (There are a few other moments where the authors take artistic license with history, which can be a bit grating if you are familiar with the history.) Finally, it seems that the authors didn't know how to end the novel; Logicomix fades away in a highly unsatisfying way.

That said, I am very very happy that Logicomix is finally in print. I am waiting for the sequel.

Defunctionalizing proofs (revised + extended edition)

2009-07-10T02:32:00.000-07:00

I wrote a paper that elaborates and improves upon the basic idea I talked sketchily about some months ago, of applying defunctionalization towards a formal representation of "Ω-rules" in Twelf, with applications to pattern-matching and cut-elimination. The paper was accepted to Proof Search in Type Theory, next month in Montreal.

Text: pdf
Code: twelf
Abstract:
In previous work, the author gave a higher-order analysis of focusing proofs (in the sense of Andreoli’s search strategy), with a role for infinitary rules very similar in structure to Buchholz’s Ω-rule. Among other benefits, this “pattern-based” description of focusing simpliﬁes the cut-elimination procedure, allowing cuts to be eliminated in a connective-generic way. However, interpreted literally, it is problematic as a representation technique for proofs, because of the difficulty of inspecting and/or exhaustively searching over these infinite objects. In the spirit of infinitary proof theory, this paper explores a view of pattern-based focusing proofs as façons de parler, describing how to compile them down to first-order derivations through defunctionalization, Reynolds’ program transformation. Our main result is a representation of pattern-based focusing in the Twelf logical framework, whose core type theory is too weak to directly encode infinitary rules—although this weakness directly enables so-called “higher-order abstract syntax” encodings. By applying the systematic defunctionalization transform, not only do we retain the beneﬁts of the higher-order focusing analysis, but we can also take advantage of HOAS within Twelf, ultimately arriving at a proof representation with surprisingly little bureaucracy.

This is very much work in progress—comments much appreciated!

The Value of the Free Man

2009-07-03T19:13:00.000-07:00

I found this political lecture by Albert Einstein (delivered before "The Friends of Europe" in London) in an old magazine (World Digest, April 1934), while sorting through piles and piles of books. As far as I can tell it does not exist online, so I transcribed it and am placing it here (and here):

The Value of the Free Man

Modern life is worth while because the individual guaranteed the possibility of free development, free communication, free religion, and, as far as the well-being of human society permits, free initiative of action.

Nobody can deny that to-day this foundation of a worthy existence is in considerable danger. Forces are at work which are attempting to destroy the European inheritance of freedom, tolerance, and human dignity. The danger is characterised as Hitlerism, Militarism, and Communism which, while indicating different conditions, all lead to the subjugation and enslavement of the individual by the State, and bring tolerance and personal liberty to an end.

When I speak of Europe, I do not mean the geographical conception of Europe, but a certain attitude of life and to society which has grown up in Europe and is characteristic of our civilisation.

I mean the spirit which was born in ancient Greece and, more than a thousand years later, at the time of the Renaissance, spread from Italy: the spirit of personal liberty and regard for the individual.

If to-day our knowledge of natural laws and the technical possibilities for the advancement of our lives have reached such perfection as never before in the known history of mankind, we owe this to the fact that only the individual can really create what is new and worthwhile.

Without such freedom there would have been no Shakespeare, no Goethe, no Newton, no Faraday, no Pasteur, and no Lister.

There would be no comfortable houses for the mass of the people, no railway, no wireless, no protection against epidemics, no cheap books, no culture and no enjoyment of art for all.

There would be no machines to relieve the people from the arduous labour needed for the production of the necessities of life.

It cannot be my task to act as judge of the conduct of a nation from the point of view of statesmen or as one who is immersed in the responsibilities and the details of the daily life of politics.

Yet everyone who loves the subtler manifestations and the beauty of the human spirit, and who believes himself able to diagnose the deeper causes of the present situation, has the duty of raising his voice in warning.

For if we do not make energetic resistance, we shall sink back into a way of life which is indistinguishable from that of the subjects of the old Asiatic despotisms.

It will be worse than theirs, for the modern despots, while not disposing of more brains than their former colleagues, own the arm---and it is a long and strong arm---of a mighty technical apparatus for the exercise of physical power, and in their schools, radio, and press they possess an instrument of mental and moral influence which ordinary mortals cannot resist.

It is of the essence of despotism not only that one individual with practically unlimited authority is at the head, but that society itself becomes the tool of the enslavement of the individual.

I would therefore much rather call the enemy of the European spirit "Servitude to the State."

This servitude exists when the State is not an instrument in the hands of the citizens, as it ought to be, but when the citizens are in practice unconditionally delivered over to the power of the State. This condition is expressed in the German language by speaking of the population as "human material" (Menschenmaterial).

What is it that converts the free European into a slave of the State? My simple answer is: the necessity of military organisation on the part of each separate State. In other words, the cause is international juridical anarchy. I believe that the German has become the complete victim of the State because his country, by its geographical condition, is most exposed to attack, and was therefore most dependent on rigid military organisation.

But military organisation means degradation of the individual to an obedient tool, void of will. It demands the training of youth into an automatic and uncritical obedience towards a superior.

In short, it implies the renunciation of personality and human worth.

The petty persons who to-day govern Germany owe their power mainly to the education of former generations in a spirit of submissiveness and servility, a state of mind which is diametrically opposed to the consciousness of personal responsibility of the true European man.

If it be true that individuality as the basis of the European ideal is gravely menaced by the necessity for military organisation of the several separate States, there can be no doubt as to how the danger may, and must be, overcome.

The separate State must be offered an effective guarantee for its security in relation to neighbouring States.

Disarmament according to a fixed plan without guarantee of security by the entire community of States is impossible, if for no other reason than that to-day war is not a society-game where one can be sure that everything will go according to rule.

On this main issue of how to win through to civilisation, therefore, I share entirely the French point of view.

I am also convinced that a universal collective guarantee for the security of individual States is in itself by no means enough.

The military organisations of the separate States ought to be internationalised, that is, transformed into an international police force subject to a super-national authority.

If the reader thinks this Utopian, he may, for comparison, imagine a State in which there are no police and no courts. In their place a law exists which makes it compulsory for every citizen to help his fellow-citizen with whom a third citizen dares to interfere. Do you believe that the citizens of such a State would desist from carrying their own weapons about with them? I doubt it.

The serious efforts of the Governments which have led to the Disarmament Conference show that there exists a general awareness of the danger in which we live. In the light of the foregoing, lack of success is not difficult to understand. There are problems which cannot be brought to solution by small steps and stages.

Either the security of States is guaranteed internationally, in which case the separate State needs no military organisation at all, or this guarantee is not achieved, in which case the State must arm as effectively and completely as possible.

Nationalism in my opinion is, in this respect, no more than an idealistic basis for the militarist and aggressive mental condition of a people.

Hitlerism is a form of State thoroughly adapted to military purposes. This is so true that a "leader" can only hold himself in power by behaving aggressively, at least in appearance, in foreign relations, for he must always hold before the eyes of his people the real or imaginary purpose for which they are asked to sacrifice their freedom.

Only through perils and upheavals can nations be brought to further developments. It is in times of economic distress such as are experienced everywhere to-day, that one sees very clearly the strength of the moral forces which reside in a people.

Let us hope that a historian, delivering judgment in some future period when Europe is politically and economically united, will be able to say that in our days the liberty and honour of this Continent were saved by its Western nations.

Let him be able to say they stood fast together against the temptations of hatred and oppression, and that the Western world defended successfully the liberty of the individual, without which life to a self-respecting man is not worth living.

The leading statesmen are burdened with tremendous responsibilities to-day as they were twenty years ago.

May they succeed through timely agreement in establishing a condition of unity and clarity of international obligations in Europe, so that to every State a war-like adventure must appear foredoomed as utterly hopeless.

But we are concerned not merely with the technical problem of securing and maintaining peace, but also with the important task of education and enlightenment. If we want to resist the powers which threaten to suppress intellectual and individual freedom, we must keep clearly before us what is at stake, and what we owe to that freedom which our ancestors won for us after hard struggles.

Thus, the work of statesmen can succeed only if it is supported by the serious and determined will of the peoples. And the essence of that will is the creative adventure of free citizens.

I know very many people who are willing to approve in principle opinions such as have been expressed here, but who will fall back the next moment into the ruts of ordinary political action.

But he who is seriously convinced that the future growth of our civilisation is bound up with the preservation and development of the human personality, must be prepared to make sacrifices for his convictions.

The sacrifice I am thinking of is the partial abandonment of State sovereignty by the separate States, and the yielding of the principle of egoism in favour of international security.

Here lies the hope of Europe and the Western world.

The Proofs of Life After Death: a 20th Century Symposium

2009-06-08T15:39:00.000-07:00

Browsing in the local history section of the Central Library in Rochester, NY, I stumbled on this curious book from 1902:

Wonderfully, the full text is available online through google books. The book is a collection of responses by various thoughtful people to the following request:

Dear Sir:

The Author of this letter, inspired by the untimely decease of a dear friend, and in contemplation of the numerous philosophical and logical theories leading to a belief in the continued existence of the soul, or personal identity after death, begs of you the great favor of a letter, setting out as briefly, or at such length as may be convenient, what you consider to be the strongest reason, or argument, advanced by science or philosophy, or by common sense, in favor of an affirmative answer to this mighty question; or preferably, a statement of your own deductions thereon.

It is our desire to obtain from thinkers and educators of the world, an expression—a twentieth century bulletin, on this subject.

Our request will impress you doubtless as an unusual one, but none the less will you see the force of it, and its possibilities. Who can measure the impetus such a compilation may have upon the inquiring human mind?

May I not have your co-operation in this matter?

Thanking you now in advance for the courtesy of a reply, I am

Fraternally yours,
ROBERT J. THOMPSON.

Wellington Ave., Chicago, U. S. A.
October, 1901.

I had fun skimming through the first collection of responses, from "The Scientists". The variety of responses is interesting. Although there's the usual bloviation on the cosmological and teleological arguments, as well as some self-citations to studies confirming the existence of telepathy and other paranormal phenomena, there's also some healthy scientific modesty. E.g., E. Ducleaux writes,

Excuse me for not being able to help you in your investigation. I have no scientific opinion regarding the questions you put. I mean, no opinion that rests on anything but personal beliefs. Besides, I think that everybody is in about the same position and that any reasons that may be brought forth in favor of one's opinion are only good for the person that brings them forth, and that they cannot impress the listener; they are therefore not scientific reasons.

D. I. Mendélieff's response begins similarly, although he ends by arguing for the immortality of the soul by analogy with the laws of conservation of mass and energy (an analogy I was surprised to see repeated very often in the other responses!):

The question as to the continuance of the existence of the soul or personal identity after death, mentioned in your letter of August, 1901, I, as a natural philosopher, consider to be an hypothesis which cannot be proved by evidence of real facts. But as a man educated in a religious sense, I prefer to remain in the belief of the immortality of the soul. It is my opinion that the philosophical side of the question consists in the relation between the soul, the natural forces, and matter; and if it were possible to clear up to some extent this feature of the problem---the relation between force and matter---then also the relation between the soul and natural forces would be forwarded to a great extent.

The unquestionable existence of reason, will and consciousness compels us to acknowledge the existence of a special world of relations of this kind, and any rational conclusion in relation to this special world cannot be accepted as proved quite in the same manner. Knowledge of physics and mechanics does not give anything in relation to chemistry or in relation to the existence of celestial bodies.

We must simply confess that it is impossible to comprehend this question in a general way, but it would also be sheer nonsense to ignore the physical world; and as matter and natural forces must be acknowledged as eternal, it is also probable that the soul is eternal.

But my favorite response was by James R. Nichols, marveling at the modern-day wonders of ~~Web 2.0~~ the telephone:

Do we not every day converse with unseen friends long distances away; do we not recognize their familiar voices, in homes separated from us by rivers, woods, and mountains? These voices come out of the darkness, guided by a frail wire which science provides as a pathway.
[...]
If our friends in this life, dead to us (hidden as they are by the shroud of space), can be seen, and we can hear their voices, their shouts of laughter, the words of the hymns they sing, the cries of the little ones in the mother's arms, is it very absurd to anticipate a time when those dead to us by the dissolution of the body may, by some unknown telephony, send to us voices from a realm close at hand, but hidden from mortal vision?

The Logical Basis of Evaluation Order and Pattern-Matching

2009-05-08T10:11:00.000-07:00

The Logical Basis of Evaluation Order and Pattern-Matching

An old and celebrated analogy says that writing programs is like proving theorems. This analogy has been productive in both directions, but in particular has demonstrated remarkable utility in driving progress in programming languages, for example leading towards a better understanding of concepts such as abstract data types and polymorphism. One of the best known instances of the analogy actually rises to the level of an isomorphism: between Gentzen's natural deduction and Church's lambda calculus. However, as has been recognized for a while, lambda calculus fails to capture some of the important features of modern programming languages. Notably, it does not have an inherent notion of evaluation order, needed to make sense of programs with side effects. Instead, the historical descendents of lambda calculus (languages like Lisp, ML, Haskell, etc.) impose evaluation order in an ad hoc way.

This thesis aims to give a fresh take on the proofs-as-programs analogy---one which better accounts for features of modern programming languages---by starting from a different logical foundation. Inspired by Andreoli's focusing proofs for linear logic, we explain how to axiomatize certain canonical forms of logical reasoning through a notion of pattern. Propositions come with an intrinsic polarity, based on whether they are defined by patterns of proof, or by patterns of refutation. Applying the analogy, we then obtain a programming language with built-in support for pattern-matching, in which evaluation order is explicitly reflected at the level of types---and hence can be controlled locally, rather than being an ad hoc, global policy decision. As we show, different forms of continuation-passing style (one of the historical tools for analyzing evaluation order) can be described in terms of different polarizations. This language provides an elegant, uniform account of both untyped and intrinsically-typed computation (incorporating ideas from infinitary proof theory), and additionally, can be provided an extrinsic type system to express and statically enforce more refined properties of programs. We conclude by using this framework to explore the theory of typing and subtyping for intersection and union types in the presence of effects, giving a simplified explanation of some of the unusual artifacts of existing systems.

Successfully defended April 17, 2009!

On the meaning of logical completeness

2009-02-04T21:59:00.000-08:00

I would really like to have time to read this paper by Michele Basaldella and Kazushige Terui, as well as many of Terui's other highly interesting recent papers.

Defunctionalizing Proofs (and how to define a pattern-matching, CPS language in Twelf)

2009-01-26T19:55:00.000-08:00

I drove back from Savannah and POPL/PLPV/TLDI yesterday. It was a long and exciting drive (in part because of the snow and frozen windshield washer fluid driving through West Virginia, god I hate that stretch of highway), and a long and exciting week at the conference. My favorite talk was an invited one by Chris Barker on Wild Control Operators, in the sense of "continuations in the wild". Chris is a linguist who for several years (I think since around 2000) has been advocating the use of continuations to analyze apparently non-compositional phenomena in natural language. He collaborates with brilliant computer scientist Ken Shan, who wrote his PhD thesis on "Linguistic Side Effects".

In this post I want to introduce some Twelf code I wrote after getting back to Pittsburgh. At the PLPV workshop I presented my paper on Refinement Types and Computational Duality. I didn't exactly time the talk well, and ended up going through about half my slides in ten minutes past the allotted time. (Luckily, I didn't run into Obama's talk, which was better prepared.) The paper itself is similar in that respect, trying to rush through too much material in too short a space. One of the ideas it describes probably too briefly is that of defunctionalizing proofs. Defunctionalization is a trick due to John Reynolds, from his paper on Definitional Interpreters for Higher-Order Programming Languages. It allows you to take a program with higher-order functions and convert it into one with only first-order functions. Essentially, it boils down to giving a unique tag to every function definition in your program, and then defining a separate "apply" function that tells you how to apply the function denoted by a tag to an argument. (A complication is that function bodies may reference escaping variables, so defunctionalization has to be preceded by closure conversion.)

Why would proofs contain functions in the first place? For the same reason programs do: sometimes they are a useful abstraction. An old example from proof theory comes in the work of Paul Lorenzen and Kurt Schütte, who in the 1950s began revisiting Gerhard Gentzen's work via infinitary methods (see "Lieber Herr Bernays!, Lieber Herr Gödel!" by Feferman for an interesting history). Schütte simplified Gentzen's proof of cut-elimination for Peano arithmetic by replacing the usual schema of induction by the so-called ω-rule, which says, "To prove ∀x:ℕ.A(x), prove A(0), A(1), A(2), ...". At first glance, the ω-rule seems silly: how can we ever apply a rule with infinitely many premises? But a different way of looking at the ω-rule is that it demands a single function, mapping natural numbers n to proofs of A(n). And this function can certainly have a finite representation, for example as a C program.

In some other papers, I described how to view Andreoli's "focusing" proofs as higher-order in this sense, containing functions that map proof patterns (or refutation patterns) to other sorts of proof objects. For example, to refute a proposition of positive polarity, we build a function from proof patterns to proofs of contradiction. This has a simple Curry-Howard interpretation: we can define call-by-value continuations by functions from value patterns to expressions. In other words, we actually represent the syntax of a programming language using computation.

Dependently-typed functional languages such as Agda and Coq turn out to be very convenient platforms for embedding such higher-order language definitions. In the dependently-typed setting of Twelf, frustratingly, it seems impossible! This is surprising, at least in a superficial way, because Twelf is well-known for allowing language definition via "higher-order abstract syntax" (HOAS). But HOAS is a different idea from the above technique (which I've taken to calling AHOS). Essentially, the problem is that the function space of LF (the type-theoretic core of Twelf) is very weak: abstractly, a function A→B is just a B with a hole for an A, or in other words, A→B represents a substitution function, something into which you can plug in an A to obtain a B. This weakness is in fact crucial for doing HOAS. But it means we absolutely cannot use the LF function space to do AHOS. (Think, for example, what that would mean for the ω-rule: to prove ∀x:ℕ.A(x), we would have to give a proof of A(n) that works the same way for every n. But the predicate A might hold for different n for different reasons, so such a rule would be woefully incomplete.) On the other hand, that we can't define languages using AHOS in Twelf is frustrating, because HOAS is rather nice for other parts of a language definition.

Fortunately, it turns out we can have our AHOS and eat HOAS too! And it all boils down to Reynolds' trick. You can check out the code here.

bipolarism theory

2008-12-24T14:50:00.000-08:00

Another interesting conference, on Bi-Polarism Theory and Mathematics is Inconsistent. And while you're in the holiday spirit, check out The Twelf Days of Christmas.

a conference dedicated to Per Martin-Löf on the occasion of his retirement

2008-12-04T14:16:00.000-08:00

This promises to be a very exciting conference.

lies and updates

2008-11-18T20:45:00.000-08:00

So in case you haven't realized, those promises to post more on this blog were just lies. Not gonna happen. But in the hope of generating a bit more content, and also to give this blog a more Web 2.0 feel, I've added a "google reader shared items" bar, which links to various posts by other people that I find interesting. Don't worry, there aren't plans for an AdSense bar in the near future.

A few other updates:

This past weekend there was a small workshop at CMU, Bernaysfest, dedicated to the life and work of Paul Bernays, a collaborator of David Hilbert. I snuck in, and heard a bunch of interesting talks on the history of proof theory. (Bernd Buldt's talk, listed as TBA on the schedule, was on "Mathematical practice and platonism: A phenomenological perspective", and quite interesting once I understood what he was trying to do. He wants to give an explanation for why so many mathematicians are platonists, why mathematical objects feel "real" to them, by looking at mathematics as a social process.) The workshop also brought Bill Tait, who last week gave a standing-room-only talk about cut-elimination in predicative systems (Richard Zach blogs about).
A month ago I gave a fluffy talk on "walking the way of duality" at the Student Seminar Series. Here are the slides, but I'm keeping the video to myself, thank you very much.
My refinement types paper was accepted to PLPV, as was Dan and Bob's paper, so we'll be going to Savannah.

Refinement types and computational duality

2008-07-24T06:23:00.000-07:00

Apologies that this blog hasn't seen much action for a while. Hopefully that will get fixed soon, but then again the whole thesis thing might get in the way. This post is just to say that recently I've been having fun writing up a paper:

One lesson learned painfully over the past twenty years is the perilous interaction of Curry-style refinement typing with evaluation order and side-effects. This led eventually to the value restriction on polymorphism in ML, as well as, more recently, to similar artifacts in prototype refinement type systems for ML with intersection and union types. For example, some of the traditional subtyping laws for unions and intersections are unsound in the presence of effects, while union-elimination requires an evaluation context restriction in addition to the value restriction on intersection-introduction.

This paper reexamines the interaction between refinement types and evaluation order from the perspective of computational duality. Building on recent work on the Curry-Howard interpretation of focusing proofs as pattern-matching programs written in infinitary, higher-order syntax, I give a simple explanation of intersection and union types in the presence of effects, reconstructing phenomena such as the value restriction and differing subtyping laws for call-by-value and call-by-name-- not as ad hoc artifacts, but indeed as logical theorems. However, this abstract account using infinitary syntax has the drawback that refinement checking is undecidable---to address this, I show how to systematically construct a finitary syntax via defunctionalization, and then give an algorithmic refinement checking system. Parallel to the text, a formalization in the dependently-typed functional language Agda is described, both for the sake of clarifying these ideas, and also because it was an important guide in developing them. As one example, the Agda encoding split very naturally into an intrinsic ("Church") view of well-typed programs, and an extrinsic ("Curry") view of refinement typing for those programs.

Code available here.

Today is election day...

2008-04-22T08:41:00.000-07:00

...so maybe I can post about a couple unusual things today. First: go vote! If you live in Pennsylvania, are eligible to vote, are registered with a political party, and haven't voted already. (Not sure what segment of my huge readership that applies to.) Yesterday I heard Barack Obama speak at the Petersen Events Center. The content of the speech wasn't all that exciting (since it's all been said before), but I was very impressed by the fact that he made the effort for a last-minute, late-night stop in Pittsburgh. You could see on his face just how tired he was, but also that he knew the stakes, and was determined to keep standing up. It somewhat reminded me of kibadachi practice.

Second: over the weekend I met an old friend from college, Ben Schmidt, who now studies American history at Princeton. Later I was looking at his website, and saw that he has a very interesting paper about using a variation of Google's PageRank algorithm to rank PhD programs:

Ranking Doctoral Programs by Placement: A New Method
Benjamin M. Schmidt and Matthew M. Chingos
Forthcoming in PS: Political Science & Politics

Most existing rankings of graduate programs rely on some measure of faculty quality, whether it be reputation (as in the National Research Council and US News rankings), honors (prizes, membership in learned societies, etc.), or research quality and quantity (as in citation studies and publication counts). We propose a ranking that focuses instead on the success of a program’s graduates. By using stochastic matrices, it is possible to create a system in which programs essentially “vote” for each other by hiring graduates of other programs as professors in their own department. This system allows us to create an objective, results-oriented measure that is well suited to measure the quality of departments whose graduates aspire to academic positions. The rankings correlate well with reputational ranking systems, and include a per capita measure that recognizes the accomplishments of smaller but high quality programs.

a paper

2008-04-14T15:53:00.000-07:00

Focusing on binding and computation
Dan Licata, Noam Zeilberger, and Robert Harper
To appear at LICS 08

Variable binding is a prevalent feature of the syntax and proof theory of many logical systems. In this paper, we define a programming language that provides intrinsic support for both representing and computing with binding. This language is extracted as the Curry-Howard interpretation of a focused sequent calculus with two kinds of implication, of opposite polarity. The representational arrow extends systems of definitional reflection with a notion of scoped inference rules, which are used to represent binding. On the other hand, the usual computational arrow classifies recursive functions defined by pattern-matching. Unlike many previous approaches, both kinds of implication are connectives in a single logic, which serves as a rich logical framework capable of representing inference rules that mix binding and computation.

Comments appreciated!

just wait a second...

2008-04-12T14:36:00.000-07:00

An article of faith is that the undecidability of the halting problem makes it impossible to restrict to terminating programs and still have a general-purpose programming language. On the other hand, another article of faith is that we'd be in big trouble if we allowed non-terminating proofs in mathematics (e.g., "Trust me, I have a proof of the Riemann Hypothesis, just wait a second..."). Why the double standard? Do we shackle ourselves by using a fragment of mathematics that disallows (we hope) non-terminating proofs? Or have we been too hasty to accept non-terminating programs? The latter stance is embraced in total functional programming. But I think the former is also not super crazy. With a more interactive notion of proof, potential non-termination would not be so dangerous.

Z: "I have a proof of the Riemann Hypothesis, can you add it to the Book?"

E: "Of course, but first can you tell me how you handle this tricky case?"

E presents tricky case to Z

Z: "Sure, no problem, this case is easily handled by, um, some math, er, ..."

Z stalls

E waits patiently, but keeps the Book firmly shut

In some sense, terminating proofs are just a time-saving mechanism for referees. It would indeed be a shame if Z wasted all of E's time with this pseudoproof of RH. On the other hand, E could be doing other things at the same time, such as drinking coffee, or running SETI@Home.

anglo-franco photos

2008-03-13T06:27:00.000-07:00

In Nottingham, a statue of Kevin Costner:

In London, my sister's cat Arras:

A group of angry Serbian protesters in London:

Chango Spasiuk!

The students at the Ecole Polytechnique in Lozère draw some neat murals:

Paris has a successful bike-sharing program:

The French are serious about their fast food.

The town of Antony, where I stayed with Kaustuv and Vivek, had a delightful Sunday market.

Un canard:

Indian fast food, near the Gare du Nord:

My gracious host Kaustuv:

Jean-Yves, after his first lecture on the Geometry of Interaction V:

Neither the subject nor the cameraman were prepared for this photo, hence
Paul-André came out a bit blurry. In real life, he is quite sharp!

transatlantic updates

2008-02-24T12:08:00.000-08:00

So I just arrived in Paris today. Last week I was in Nottingham at DTP, then visiting my sister in London. Both were awesome! In my talk at DTP, I began with some ludics propaganda, then tried to walk the audience through how to encode focusing with higher-order rules in Agda (and extract a functional programming language with explicit evaluation order and pattern-matching). You can check out the annotated agda code. I also had/overheard lots of great conversations, in particular Sebastian Hanowksy taught me some fascinating things about synthetic topology and the delay monad, and Anton Setzer/Peter Hancock piqued my interest in going back to Buchholz's work about the ω/Ω-rule. The highlight of the London visit was probably seeing Chango Spasiuk.

This week I'll be meeting with Paul-André Mellies, and giving talks at PPS and LIX.

Fun with polarity and unicode

2008-01-30T13:21:00.000-08:00

> 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.

[0] : 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.List
open 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)))))

Back from POPL, forward to AGDA

2008-01-14T20:19:00.000-08:00

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.

lucidity vs ludicity, and translating one esoteric language into a slightly less esoteric one

2007-11-18T21:35:00.000-08:00

One of the things I often wonder about is how to say things that are intelligible. Too frequently, I lapse into jargon─sometimes even on-the-spot-invented jargon─and only realize this after the damage has been done. An example: the previous blog post, which was probably incomprehensible to all but...well, probably to all. I promise I will try hard to avoid doing this in the future.

But on the topic of making things less inscrutable─and not on the topic of Girard!, though keep your eyes on the Girard Reading Group Wiki─another thing I've been thinking about is how to translate Martin-Löf's "judgment vs proposition" distinction (as spelled out in the Siena Lectures) into the language of category theory. At first, the judgment vs proposition distinction may seem pedantic: okay, one can distinguish between a well-formed proposition "A" and the assertion that it is true "A true"...but so what? Well, the distinction helps get dependent type theory off the ground, since well-formedness is defined mutually with truth (the dependent quantifier ∏x:A.B is a well-formed proposition if and only if A is well-formed and B is well-formed under the assumption x:A). More mundanely, it is obvious that a separate notion of judgment is useful if we want to refute propositions as well as assert them, using the judgment "A false" in addition to "A true".

Well, this is actually not quite so obvious. Why not just assert ¬A? For a philosophical explanation of why not, Greg Restall's essay "Multiple Conclusions" is a nice read. From a proof/type-theoretic perspective, the reason why not to identify "A false" with "¬A " is that we need the separate judgment in order to obtain "good compositionality" principles─this is an informal but very general law gleaned by Frank Pfenning and collaborators over years of refining the "judgmental method", to which the paper "A judgmental reconstruction of modal logic" probably serves as the most complete introduction. Unfortunately, though, my impression is that these principles are still not very widely accepted or understood.

I think part of the problem is the seemingly obscure philosophical origins of the judgmental method (although its application is practically motivated), and so what I would like is a translation guide into the language of category theory (an order of magnitude less obscure, though granted still sometimes considered esoteric) . I think there must be such a translation, since the whole point of the judgmental method (at least in my mind) is obtaining compositionality principles.

Does anyone know if the judgment vs proposition distinction has been explored before in category theory? As a simple example of a system with two judgments that should be possible to explain categorically, I propose the bidirectional lambda calculus with implication and conjunction (described in Section 3.1 here).

Location: PHI Bar

2007-11-06T18:38:00.000-08:00

(Only the location matters.)

Today we had the second (or really 1.5th) meeting of the Girard Reading Group, a.k.a. the Locus Solum Drinking Group. Many more people than I expected! It seems that obscure proof theory is a sexy topic. We're trying to go through Locus Solum systematically, although it's hard because the writing style makes digression so tempting. Fortunately, it's a diverse enough group of people that we better stay disciplined or else anarchy will ensue (as in the first meeting). Rob put up a wiki for us to pool whatever nuggets/maggots of wisdom we manage to extract. Stay tuned there for updates! Here I'll talk about a few of today's punchlines (these will probably go on the wiki soon).

I think it was a pretty productive day. We made it through the basics of designs-dessins, and started to talk about designs-desseins (what's the differance between them?). Basically, designs-dessins are focused sequent calculus proofs in affine, polarized linear logic, where formulas have been replaced by loci. I still don't have a good sense of the motivation for locativity, but the definition is very concrete: a locus ξ is just a finite sequence of natural numbers. Appending a number ("bias") i corresponds to taking an immediate subformula (ξ*i is an "immediate sublocus" of ξ). There are two kinds of sequents ("pitchforks"): ⊢ Λ (positive pitchfork) and ξ ⊢ Λ (negative pitchfork). Here Λ is a finite set of loci.

Now, Girard doesn't much intuition for what these judgments mean, but my running interpretation is as follows: a positive pitchfork asserts that all of the the loci in Λ can't be false, i.e. that if all the loci in Λ are false we have a contradiction; a negative pitchfork asserts that if all the loci in Λ are false, then ξ is also false. (I'm not really sure what it means for a locus to be false, as opposed to a formula, but let's run with it...) Observe this is just an inversion of the usual interpretation of intuitionistic sequents Γ ⊢ A and Γ ⊢∙. However, the system is not really "dual intuitionistic", because the notions "false" and "contradiction" used here are intuitionistic, and really there is a hidden notion of "direct truth" buried within the rules for proving pitchforks.

Let's take Girard's example "pre-located" formula A = (P^⊥⊕ Q^⊥) ⊗ R^⊥. There are two proper positive rules (right-rules) for A:

    
  P ⊢ Γ      R ⊢ Δ            Q ⊢ Γ      R ⊢ Δ
—————————————————————      ——————————————————————
     ⊢ Γ, Δ, A                    ⊢ Γ, Δ, A

Under our interpretation, to prove ⊢ Γ, Δ, A we must show that all of the formulas in Γ, Δ, A can't be false. These rules attempt to do this by focusing on A, i.e. they try to show that A in particular is true (still under the assumption that Γ and Δ are false). To prove A, we must prove both P^⊥⊕ Q^⊥ and R^⊥. To prove a disjunction we must prove either of the disjuncts, while proving the negation of a formula is the same as refuting it. Hence to prove A (under falsehood assumptions Γ, Δ), we must either refute P and refute R (with an arbitrary splitting of the assumptions), or else refute Q and refute R. This is exactly how we read the premises of the two rules. On the other hand, see how in one step we are able to go all the way from "show Γ, Δ, A can't all be false" to "show A is true if Γ, Δ are false" to "show either (P is false if Γ is false and R is false if Δ is false) or (Q is false if Γ is false and R is false if Δ is false)"? This is the focalization property, and it's why we didn't explicitly have to mention "truth" when we glossed the two kinds of sequents. (Editorial remark: if the truth judgment is hidden in there, though, why not show it? I.e., use a third kind of pitchfork "⊢ Λ; ξ", where ξ is already in focus. This is what I do in my paper.)

Designs-dessins are not a perfect notation for proofs, however. The problem is that not all of the loci in a pitchfork will ever be placed in focus. These loci can be split up arbitrarily among the different premises of a derivation---so we can have two dessins which apply essentially the same rules, but just differ in how they throw away these unused loci. The situation here is more or less as it is for ordinary intuitionistic logic. For any sequent calculus proof of Γ ⊢ A, we can get a "new" proof by weakening the derivation to Γ, Δ ⊢ A. However, the sequence of rules applied in both proofs is the same. Natural deduction/simply-typed lambda calculus get rid of these artificial distinctions between proofs: we can give one lambda term corresponding to both sequent calculus proofs (it simply won't mention the extra hypotheses in Δ). So designs-desseins are something like a lambda calculus for focused proofs. Yes, we should expect them to look something like spine form and pattern-matching...but we might have to squint pretty hard...

Synthetic topology

2007-07-31T13:38:00.000-07:00

I've started reading about Martín Escardó's "synthetic topology", which seems closely related to (but not quite the same as) the ludics topological interpretation. The basic idea is that rather than topologizing a language by first specifying a partial order on data, then constructing open sets using that order, and finally showing that all definable functions are continuous—the approach in traditional domain theory—instead one starts at the end and simply declares continuous functions to be those definable in the language. An open set U of a datatype D is now defined by a continuous function χ_U : D → S from D into the Sierpinski space S. In classical topology, the Sierpinski space is simply the two point set {⊤, ⊥}, with open sets {{⊤, ⊥}, {⊤}, ∅}. In synthetic topology, S is a datatype with the single element ⊤; a computation of type S can either evaluate to ⊤, or else diverge, which is represented by ⊥. So the Sierpinski space essentially represents the observable results of computation, where we only distinguish between termination and non-termination. (In ludics, these two observable results are called daimon and faith.)

So again, an open set U of D is defined by U = χ_U^-1(⊤), where χ_U : D → S is definable in the underlying programming language. It follows immediately that U is closed under contextual equivalence, i.e. if d∈U and d ≈ d' then d'∈U. However, it is not necessarily the case that the collection of open sets is closed under (infinite or even finite) unions (as in classical topology). For this to be the case, given any two functions f,g : D → S, we have to be able to construct an h : D → S such that h(d) = ⊤ iff either f(d) = ⊤ or g(d) = ⊤. In other words, our language needs a sort of "parallel-or" construct.

I haven't gotten much further yet, but this looks interesting. Also, it seems that Escardó isn't just interested in applications to programming semantics, but in examining more traditional topological questions through synthetic topology.

A tutorial: "Synthetic topology of data types and classical spaces" by Martín Escardó.

A paper: "Operational domain theory and topology of sequential programming languages" by Martín Escardó and Weng Kin Ho.

A topology of cut-elimination

2007-06-28T20:53:00.000-07:00

One of the central ideas of Ludics is an orthogonality relationship between proofs and refutations, which says, essentially, that they can be "successfully" cut against each other. Recall that Gentzen's cut rule is a method of composing derivations:

Γ ⊢ Δ, A      Γ, A ⊢ Δ
———————————————————————
Γ ⊢ Δ

The rule gives a derivation of Γ ⊢ Δ from derivations of weaker sequents, using A as an intermediary. Gentzen proved that the cut rule is unnecessary, i.e. that it is always possible to obtain a direct derivation of Γ ⊢ Δ without going through the middle-man. However it turned out that this process of cut-elimination was of extreme interest.

In "Locus Solum", Girard tells us to focus our attention on the following instance of cut:

 ⊢ A      A ⊢
——————————————
⊢

In words: "From a proof of A and a refutation of A, derive contradiction." But isn't that a vacuous instance of cut? Logic is supposed to be consistent, so how could we ever have both a proof and a refutation of the same proposition? Well, Girard's solution is to add a single rule, the daimon, that can conclude anything from no premises:

——————
Γ ⊢ Δ

Since the logic becomes inconsistent, it is now entirely possible to have both a proof and a refutation of the same proposition. But isn't that...crazy? Perhaps Girard inhaled a bit too much mustard before coming up with this stuff?

But actually, if we think of cut-elimination in terms of the Curry-Howard correspondence, the daimon makes a good deal of sense. A proof of A corresponds to a value of type A (in the ordinary programming languages sense), while a refutation of A corresponds to a continuation accepting type A. (Strictly speaking, in Ludics proofs don't correspond to values in the ordinary sense, but for now we can ignore the difference.) Now, what can a continuation K do with a value V:A? Well, V might itself contain suspended continuations, and K could call any of those with some values. But another possibility is that K simply terminates the computation. And that's when it calls the daimon. In other words, daimon is just French for "done". Thus when Girard defines a proof and a refutation to be orthogonal when their cut normalizes to the daimon, this is another way of saying that we can throw a value to a continuation and get a terminating result (notation: V⊥K).

So what does this have to do with topology? For any type A, let's collect all of its values into a set X_A = {V | V:A}. Now, let K be any A-accepting continuation. We can use K to pick out a subset of X_A, namely the set of values on which K terminates. That is, we build the set K^⊥= {V:A | V⊥K}. And then we define a topology Ω_Aon X_A, generated by all of the basic open sets K^⊥.

Let's try to see how this works for the type of booleans, with set of values X₂ = {t, f}. We can describe any boolean continuation as essentially fitting one of the following four recipes:

[t|f ↦ done]

[t ↦ done]         [f ↦ done]

[]

The top recipe ([t|f ↦ done]) describes a continuation which, given either t or f, simply returns. The next recipe on the left ([t ↦ done]) describes a continuation which returns on t, but whose behavior is unspecified (and thus possibly non-terminating) on f. Similarly with [f ↦ done]. Finally, [] is the boolean continuation with totally unspecified behavior. It is easy to see the basic open set corresponding to each continuation:

{t,f}

{t} {f}

{}

And so Ω₂ is simply the discrete topology. In general, though, the topology Ω_A will be more complicated.

Fact: Ω_A is T₀.

Expanding the definition of Ω_A and of the separation axiom, this means that for any two "syntactically distinct" values of type A (omitting the precise definition), there is some continuation which terminates on one but not the other. Or in programming language terminology, T₀ says that syntactic inequality implies contextual inequivalence.

Fact: Ω_A is not always T₁.
Counter-example: Consider Ω_¬2, the topology on boolean continuations treated as values. We treat a continuation as a value by wrapping it in con, so for example con([t ↦ done]) is a value of type ¬2. Now, we can again summarize the behavior of any ¬2-continuation, this time with five possibilities:

[con(k) ↦ done]

[con(k) ↦ k(t)]         [con(k) ↦ k(f)]

[con(k) ↦ k(t)∥k(f)]

[]

The top continuation simply ignores its argument and returns. The next two call k with a single boolean, either t or f. The continuation on the third line calls k with both t and f. And finally, the behavior of the continuation [] is, again, unspecified. Now let us use the shorthand {t,f}, {t}, {f}, {}, to refer to the four previously-defined boolean continuations in the evident way. Then the above ¬2-continuations generate the following basic open sets:

{{t,f},{t},{f},{}}

{{t,f},{t}} {{t,f},{f}}

{{t,f}}

{}

Then, for example, {t} and {t,f} cannot be separated, since the latter is in every open set containing the former. Another way of putting this is that any context in which the value con([t ↦ done]) is acceptable, the value
con([t|f ↦ done]) is also acceptable; the former supplies a continuation guaranteed to terminate only on t, the latter one that that will terminate on any boolean. It might also be worth noting that the two values con([t ↦ done])and con([f ↦ done]) are separable, but not by open neighborhoods.

Okay! Hopefully that's a reasonable sketch of the basics of the topological interpretation in Ludics. Stay tuned for more...

Preliminaries

2007-06-10T13:39:00.000-07:00

The premise of this blog is first: wow, I have a blog! Second, I feel that at this point in my life I need to spend less time thinking up crackpot ideas, and more time writing up crackpot ideas.

Additional introduction: I am a grad student at Carnegie Mellon, with broad interests in programming languages and proof theory, logic, categories and philosophy of language. More specifically, my thesis work has started to take shape after a couple years spent trying to make sense of nonsense, and I might devote a few blog entries to this exegesis (hence the blog title). At the moment, many other people are pursuing similar ideas, some from very different backgrounds, and I might also spend some time trying to tie the threads. Otherwise, as I said, there will be lots of personal crackpot ideas, and alliteration.