Leibniz Equality, Decomposition, and Definability
In any interesting logic, there are propositions which are true but not provable. The same goes for intuitionistic logic. By the Curry-Howard correspondence, there are types for which neither the types themselves nor their negations are inhabited in the typed lambda calculus. An example of this is Peirce's law: ∀ p, q . ((p -> q) -> p) -> p. We can use Heyting algebra to show that Peirce's law is not provable in intuitionistic logic. According to John C. Mitchell's Foundations for Programming Languages, problem 4.3.16, we could also show that this is not provable because:
. . . if there us a closed lambda term M:((a -> b) -> a) -> a then there is a closed normal form (the normal form of M) of this type. Show that this implicational formula is not provable by showing there is no closed normal form term of this type.
In Emir Pasalic's PhD thesis, (end of section 4.2.2, page 80 in the PDF, 70 in print), he mentions that it is unknown whether the following type is inhabited:
∀ a, b, c, d . Equal (a,b) (c,d) -> Equal a cwhere type equality is defined by Leibniz equality
data Equal a b = Equal (∀ f . f a -> f b)To avoid dealing with datatypes or pairs, this can be expanded to
∀ a, b, c, d .
(∀ f . f (∀ r . (a -> b -> r) -> r) -> f (∀ s . (c -> d -> s) -> s))
->
(∀ g . g a -> g c)
In GADTless Programming in Haskell 98 (Section 6, top of page 13) Martin Sulzmann and Meng Wang call this the decomposition law.
Is there some Heyting algebra for higher-order polymorphic typed lambda calculi that we can use to show that this type is uninhabited?
14 comments:
I don't know what that means!!
No, seriously, I don't know what that means. I hate my life.
Could you please write about kittens or balloons so I can read your blog?
Sincerely,
Grover
You should start an architecture blog, and then I'll leave the exact same comment. :-)
Anyway, here's my attempt:
"In any interesting kitten, there are balloons which are true but not kittens. The same goes for balloon animals. By the Three Stooges correspondence, there are pretty, pretty flowers for which neither the kittens themselves nor their owners are rhyming in the typed balloon-animal calculus …"
Got it, thanks!
Don't you need biimplication for Leibniz equality?
Do you mean that the type should be (∀ f . f a <-> f b)? If so, then the answer to your question, which I think is a good one, is no. In Coq:
Definition leibniz (a b:Prop) : Prop := forall f:Prop -> Prop, f a -> f b.
Theorem symm: forall a b, leibniz a b -> leibniz b a.
Proof.
unfold leibniz.
intros a b eq g.
apply eq.
clear.
auto.
Defined.
Print symm.
Theorem biimplication_unnecessary: forall a b, leibniz a b -> (forall g, g a <-> g b).
Proof.
intros a b eq g.
split.
apply eq.
apply symm.
auto.
Defined.
Print biimplication_unnecessary.
You can also see this proof/code on page 5 of GADTless programming in Haskell 98.
Thanks for the reference - I can't read Coq scripts, so it was definitely helpful.
{-# LANGUAGE Rank2Types, TypeOperators #-}
newtype a :=: b = Proof { coerce :: forall f . f a -> f b }
refl :: a :=: a
refl = Proof id
newtype Flip f a b = Flip { unFlip :: f b a }
symm :: a :=: b -> b :=: a
symm p = unFlip (coerce p (Flip refl))
I wonder whether Leibniz equality of types in a constructive logic is really the same as the debated "Identity of indiscernibles" from Leibniz:
http://en.wikipedia.org/wiki/Identity_of_indiscernibles
I think the two are different because in a constructive logic the only normalized Leibniz-equality proof term is `Proof id :: a :=: a`, isn't it?
I'm sorry for my OT-ness, but Google turns up no article really explaining Leibniz equality and you're clearly knowledgeable. My best reference is the paper you cited and the one cited here:
http://scalaz.github.com/scalaz/scalaz-2.9.1-6.0.4/doc.sxr/scalaz/Leibniz.scala.html
As to whether "in a constructive logic the only normalized Leibniz-equality proof term is `Proof id :: a :=: a`, isn't it?", I can't say. That's beyond by knowledge of the subject.
As far as references, I would suggest Google Scholar for this: It found 546 articles for "Leibniz Equality" when I searched just now.
I hope you'll post another comment with the results of your search! Good luck!
Thanks for your tip. I didn't find a direct answer, but I think I can prove it.
* A Leibniz equality of a and b can convert f a to f b for any type constructor f, in particular when f is Lambda dummy -> c for arbitrary type c:
newtype Const a dummy = Const { unConst :: a }
proof :: (a :=: b) -> (forall c. c -> c)
proof p = unConst . coerce p . Const
In System F_omega, we wouldn't need newtype constructors, so we can erase Const and unConst to the identity.
The above takes a proof term of Leibniz equality and converts it to a value of type forall c. c -> c — by parametricity, that can only be the polymorphic identity function.
A better proof can be done in with (optionally) explicit type application and abstraction - say, in Agda:
data _:=:_ (A : Set) (B : Set) : Set₁ where
Proof : (∀ {F : Set → Set} → F A → F B) → A :=: B
-- _:=:_ is Agda's syntax for defining operators.
toPolyId : ∀ {A B} → (A :=: B) → ∀ {C} → C → C
toPolyId (Proof p) = λ {C} → p {λ dummy → C}
In words, toPolyId is a polymorphic function over type C, apply Leibniz equality to f = Lambda dummy -> C, get a value of type C -> C, and then generalize over c to get a polymorphic identity function.
* "Extensionality versus Constructivity". That paper shows constructively (as lemma 2.1) that Leibniz equality is equivalent to intensional equality, defined via the only constructor refl: \forall A : Type. \forall a : A. a = a. (The syntax is Agda-inspired). On proofs of intensional equality, a similar result is trivial: such proofs can only normalize to refl A a for some a \in A, since that's the only data constructor available.
Finally, this normalized proof term can be converted back to a proof of Leibniz equality; using the definition of K (see below), we see that the proof is indeed an identity function. That's however not a proof of my statement, but is still interesting.
* That paper takes its definition of intensional equality from Chapter 8 of http://intuitionistic.files.wordpress.com/2010/07/nordstrom-et-al-programming.pdf, but does not copy it in full; the reference it gives cannot be found by Google scholar, but I came across that link by accident later. Note that K in the above paper is called idpeel here.
Back to your original question: here Oleg Kiselyov answers your question in nowadays Haskell:
http://okmij.org/ftp/Computation/extra-polymorphism.html#injectivity
However, right after he links to a page showing that the extensions he uses allow deriving an inconsistency:
http://okmij.org/ftp/Haskell/impredicativity-bites.html
So I guess it's impossible to carry over that answer to any intuistionistic logic.
BTW, I remember a discussion on the Agda mailing lists, where IIRC injectivity of type constructors was used to derive a contradiction - maybe that's related? Link below
https://lists.chalmers.se/pipermail/agda/2010/001530.html
I don't feel like that proof of Leibniz equality's symmetry really helps much. Personally, I had to stare at it for a few minutes (first thinking the Coq type checker had gone mad, then thinking I had) before I understood what the "apply eq" was actually doing.
Since this is one of the first Google results for "Leibniz equality", I figured maybe I could give a more detailed proof.
Firstly, since Leibniz equality can hold between any two things (and Prop-> Prop is confusing in context) let's let our things be of any Type T:
Definition leibniz {T:Type} (a b : T) : Prop := forall f:T -> Prop, f a -> f b.
Now for our symmetry proof:
Theorem symm: forall (T:Type) (a b : T), leibniz a b -> leibniz b a.
Proof.
intros T a b LEq.
unfold leibniz in *.
intros g.
specialize (LEq (fun x => g x -> g a)).
simpl in LEq.
apply LEq.
intros.
assumption.
Qed.
The "specialize" line is the one that needs explaining. Basically, I have a hypothesis that for any proposition f, f a implies f b. Okay, let's let f(x) = (g(x)-> g(a)). Then f(a) = (g(a) -> g(a)) and f(b) = (g(b) -> g(a)). The first part is trivial, and the second is what we wanted to prove, so we're done.
The idea here is that our arbitrary "f" can *be* g(x) -> g(a) (or even forall g, g(x) -> g(a)), which allows us to reverse the equality.
Hopefully this is helpful to some readers.
Post a Comment