9
$\begingroup$

So, this is where I'm at so far:

  1. Heyting algebras model propositional intuitionistic logic (IL)
  2. so do Cartesian closed categories which also model the simply typed lamda calculus
  3. co-Heyting algebras model propositional co-intuitionistic logic (co-IL) and ??
  4. Locally Cartesian closed categories model dependent type theory (TT)
  5. Locally (and not) co-Cartesion co-closed categories model ?what exactly?

I became interested in co-Heyting algebras because of mereology for linguistics but then I learned that they model co-IL. I found a proof theory using a single-assumption multiple-conclusion natural deduction that works well as a refutation calculus dual to IL. This led me to a few questions which I can't find much research on (and I don't know much category theory.)

  1. Are there any term assignments for co-IL? What exactly would be "the construction c [that] refutes A −< B iff c [which]is a general method of construction such that applied to a hypothetical construction a that refutes A, c(a) refutes B"?
  2. Can one generalize to first-order quantifiers and if so, what do they look like? Would it be the coproduct that takes on some more computational meaning rather than how product does in TT?
$\endgroup$
5
  • $\begingroup$ "STLC". Sorry, I'm drawing a blank. What is this? The question is hard for me to understand because I don't know what co-IL is supposed to mean beyond formally dualizing IL. $\endgroup$ – Todd Trimble Sep 23 '17 at 0:08
  • 1
    $\begingroup$ STLC = simply typed lambda calculus. I linked to a page which has several papers on the proof theoretic semantics of the result of the formal dualization: in that case it provides a calculus of refutation, i.e. "proofs" of denials rather than assertions. I believe there are other semantics out there including topological semantics. What I'm looking for is a corresponding simple type theory for the prop case and what the result would be when extending it and what that TT might be. I'm thinking it's not just something with "co-exponential" objects and reversed 'eval' but I dont know $\endgroup$ – Anthony Sep 23 '17 at 0:28
  • $\begingroup$ Well, it's not true that an arbitrary ccc models simply typed lambda calculus, since simply-typed means just one (non-terminal) object. Maybe you should say "typed lambda calculus" instead. A topological semantics for propositional co-IL would be the co-Heyting algebra of closed sets of a topological space. $\endgroup$ – Todd Trimble Sep 23 '17 at 0:48
  • 2
    $\begingroup$ @ToddTrimble actually, "simply typed" allows many types/objects; the meaning of "simple" is in contrast to "dependent". The single type/object case is called "untyped" or "unityped". $\endgroup$ – Mike Shulman Sep 23 '17 at 5:09
  • $\begingroup$ @MikeShulman Oops. Thanks for the reminder. $\endgroup$ – Todd Trimble Sep 23 '17 at 9:52
1
$\begingroup$

Hey I'm not really a mathematician but I struggled with this myself.

There are more than a few ways to do this but I don't think there's really any standard notation.

Interpret typed lambda calculus backwards

The typed lambda calculus can be mapped to cartesian closed categories. We can also map it to the opposite of co cartesian closed categories.

Instead of the (negative) rules for tuples.

$$ \frac{\Gamma \vdash x : A , \Gamma \vdash y : B}{\Gamma \vdash \langle x , y \rangle : A \times B} $$

$$ \frac{\Gamma \vdash x : A \times B}{\Gamma \pi_1 x: A} $$

We have the rules for sums:

$$ \frac{\Gamma \vdash x : A , \Gamma \vdash y : B}{\Gamma \vdash [ x ; y ] : A + B} $$

However, we have to interpret the environment as a sum of variables instead of a product of variables.

If we have two patterns/case statements/contravariant functors we can sum them together.

$$ \frac{\Gamma \vdash x : A + B}{\Gamma \, \mathbb{left} \,x: A} $$

If we have a pattern match patterns/case statements/contravariant functor matching a sum type we can contravariantly make it more specific.

In a similar manner coexponential types are dual to exponential types.

$$ \frac{ \Gamma , x : A \vdash e : B}{\Gamma \vdash \, \mathbb{adbmal} \, x : A . e : B - A } $$

$$ \frac{ \Gamma \vdash f : B - A , \Gamma \vdash x : A}{\Gamma \vdash \, f x : B } $$

Interpreting everything backwards works but it's just really really confusing.

Directly work with the categorical point-free combinators

Just have the usual sum types and

$$ \mathbb{councurry} : \mathbb{Hom}(A - C, B) \rightarrow \mathbb{Hom}(C, A + B) $$ $$ \mathbb{cocurry} : \mathbb{Hom}(C, A + B) \rightarrow \mathbb{Hom}(A - C, B) $$

This is kind of nice sometimes but really I miss variables.

Reverse the categorical kappa/zeta decomposition

I wanted a nicely categorical language but with also nice variables so I found Decomposing typed lambda calculus into a couple of categorical programming languages In Proc. 6th International Conference on Category Theory and Computer Science (CTCS'95), Springer LNCS 953 (1995) 200-219

Pretty directly you get a sort of continuation passing style

Reversing (the positive tuple rules)

$$ \frac{\Gamma , x : 1 \rightarrow A \vdash e : B \rightarrow C }{\Gamma \vdash \kappa \, x : 1 \rightarrow A . e : A \times B \rightarrow C } $$

to

$$ \frac{\Gamma , x : A \rightarrow 0 \vdash e : C \rightarrow B }{\Gamma \vdash \mathbb{cokappa} \, x : A \rightarrow 0 . e : C \rightarrow A + B } $$

$$ \frac{\Gamma \vdash x : A \rightarrow 0}{\Gamma \vdash \mathbb{colift} \, x : A + B \rightarrow B } $$

You can kinda interpret this as like a case statement. It's still pretty confusing though.

Coexponentials become something like

$$ \frac{\Gamma , x : A \rightarrow 0 \vdash e : C \rightarrow B }{\Gamma \vdash \mathbb{cozeta} \, x : A \rightarrow 0 . e : A - C \rightarrow B } $$

$$ \frac{\Gamma \vdash x : A \rightarrow 0}{\Gamma \vdash \mathbb{copass} \, x : B \rightarrow B - A } $$

It's maybe a little clearer but still pretty awful.

Summary

Just do intuitionistic logic but in reverse.

Yeah I don't really have any better ideas. Currently I'm trying to figure out the positive polarity presentation of functions. My guess is that finding dual of the positive presentation might be cleaner. I'm also still looking at the dependently typed setting. I'm going to try to reverse the calculus of constructions after I look at it enough.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.