tag:blogger.com,1999:blog-6839602.post8690048312906662507..comments2017-03-09T15:26:17.288-08:00Comments on Everyone Else is Crazy: Leibniz Equality, Decomposition, and DefinabilityJim Applehttp://www.blogger.com/profile/11080395413026172939noreply@blogger.comBlogger14125tag:blogger.com,1999:blog-6839602.post-10370698814972710312017-03-09T15:23:31.632-08:002017-03-09T15:23:31.632-08:00This comment has been removed by the author.Georgehttp://www.blogger.com/profile/10685157351245616162noreply@blogger.comtag:blogger.com,1999:blog-6839602.post-20543371120115951872014-12-25T11:41:27.691-08:002014-12-25T11:41:27.691-08:00I don't feel like that proof of Leibniz equali...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.<br /><br />Since this is one of the first Google results for "Leibniz equality", I figured maybe I could give a more detailed proof.<br /><br />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:<br /><br />Definition leibniz {T:Type} (a b : T) : Prop := forall f:T -> Prop, f a -> f b.<br /><br />Now for our symmetry proof:<br /><br />Theorem symm: forall (T:Type) (a b : T), leibniz a b -> leibniz b a.<br />Proof. <br /> intros T a b LEq. <br /> unfold leibniz in *.<br /> intros g. <br /> specialize (LEq (fun x => g x -> g a)).<br /> simpl in LEq.<br /> apply LEq.<br /> intros.<br /> assumption.<br />Qed.<br /><br />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.<br /><br />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.<br /><br />Hopefully this is helpful to some readers.Randnoreply@blogger.comtag:blogger.com,1999:blog-6839602.post-68783426039245559572013-01-19T14:22:31.960-08:002013-01-19T14:22:31.960-08:00Back to your original question: here Oleg Kiselyov...Back to your original question: here Oleg Kiselyov answers your question in nowadays Haskell:<br />http://okmij.org/ftp/Computation/extra-polymorphism.html#injectivity<br /><br />However, right after he links to a page showing that the extensions he uses allow deriving an inconsistency:<br /><br />http://okmij.org/ftp/Haskell/impredicativity-bites.html<br /><br />So I guess it's impossible to carry over that answer to any intuistionistic logic.<br /><br />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<br /><br />https://lists.chalmers.se/pipermail/agda/2010/001530.htmlPaolo G. Giarrussohttp://www.blogger.com/profile/04485097839438234853noreply@blogger.comtag:blogger.com,1999:blog-6839602.post-86967502427066781312012-12-30T13:39:07.911-08:002012-12-30T13:39:07.911-08:00Thanks for your tip. I didn't find a direct an...Thanks for your tip. I didn't find a direct answer, but I think I can prove it.<br />* 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:<br /><br />newtype Const a dummy = Const { unConst :: a }<br />proof :: (a :=: b) -> (forall c. c -> c)<br />proof p = unConst . coerce p . Const<br /><br />In System F_omega, we wouldn't need newtype constructors, so we can erase Const and unConst to the identity.<br /><br />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.<br /><br />A better proof can be done in with (optionally) explicit type application and abstraction - say, in Agda:<br /><br />data _:=:_ (A : Set) (B : Set) : Set₁ where<br /> Proof : (∀ {F : Set → Set} → F A → F B) → A :=: B<br /><br />-- _:=:_ is Agda's syntax for defining operators.<br /><br />toPolyId : ∀ {A B} → (A :=: B) → ∀ {C} → C → C<br />toPolyId (Proof p) = λ {C} → p {λ dummy → C}<br /><br />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.<br /><br />* "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.<br /><br />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.<br /><br />* 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.Paolo G. Giarrussohttp://www.blogger.com/profile/04485097839438234853noreply@blogger.comtag:blogger.com,1999:blog-6839602.post-51339933629833036202012-12-29T07:58:01.538-08:002012-12-29T07:58:01.538-08:00As to whether "in a constructive logic the on...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.<br /><br />As far as references, I would suggest Google Scholar for this: It found 546 articles for "Leibniz Equality" when I searched just now.<br /><br />I hope you'll post another comment with the results of your search! Good luck!Jim Applehttp://www.blogger.com/profile/08786809982674511039noreply@blogger.comtag:blogger.com,1999:blog-6839602.post-8908026178526126512012-12-29T05:25:55.137-08:002012-12-29T05:25:55.137-08:00Thanks for the reference - I can't read Coq sc...Thanks for the reference - I can't read Coq scripts, so it was definitely helpful.<br />{-# LANGUAGE Rank2Types, TypeOperators #-}<br />newtype a :=: b = Proof { coerce :: forall f . f a -> f b }<br />refl :: a :=: a<br />refl = Proof id<br /><br />newtype Flip f a b = Flip { unFlip :: f b a }<br />symm :: a :=: b -> b :=: a<br />symm p = unFlip (coerce p (Flip refl))<br /><br />I wonder whether Leibniz equality of types in a constructive logic is really the same as the debated "Identity of indiscernibles" from Leibniz:<br />http://en.wikipedia.org/wiki/Identity_of_indiscernibles<br /><br />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?<br /><br />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:<br />http://scalaz.github.com/scalaz/scalaz-2.9.1-6.0.4/doc.sxr/scalaz/Leibniz.scala.htmlPaolo G. Giarrussohttp://www.blogger.com/profile/04485097839438234853noreply@blogger.comtag:blogger.com,1999:blog-6839602.post-52279815799336766492012-12-28T21:55:37.029-08:002012-12-28T21:55:37.029-08:00Do you mean that the type should be (∀ f . f a <...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:<br /><br /><b>Definition leibniz (a b:Prop) : Prop := forall f:Prop -> Prop, f a -> f b.<br /><br />Theorem symm: forall a b, leibniz a b -> leibniz b a.<br />Proof.<br /> unfold leibniz.<br /> intros a b eq g.<br /> apply eq.<br /> clear.<br /> auto.<br />Defined.<br /><br />Print symm.<br /><br />Theorem biimplication_unnecessary: forall a b, leibniz a b -> (forall g, g a <-> g b).<br />Proof.<br /> intros a b eq g.<br /> split.<br /> apply eq.<br /> apply symm.<br /> auto.<br />Defined.<br /><br />Print biimplication_unnecessary.</b><br /><br />You can also see this proof/code on page 5 of <a href="http://www.cs.ox.ac.uk/files/3060/gadtless.pdf" rel="nofollow">GADTless programming in Haskell 98</a>.Jim Applehttp://www.blogger.com/profile/08786809982674511039noreply@blogger.comtag:blogger.com,1999:blog-6839602.post-32016756425923272622012-12-26T04:48:22.460-08:002012-12-26T04:48:22.460-08:00Don't you need biimplication for Leibniz equal...Don't you need biimplication for Leibniz equality?Paolo G. Giarrussohttp://www.blogger.com/profile/04485097839438234853noreply@blogger.comtag:blogger.com,1999:blog-6839602.post-66949893281238080782009-12-29T04:47:05.112-08:002009-12-29T04:47:05.112-08:00This comment has been removed by the author.Vagstonhttp://www.blogger.com/profile/05936282034517218281noreply@blogger.comtag:blogger.com,1999:blog-6839602.post-34489891742747303492009-12-29T04:46:03.196-08:002009-12-29T04:46:03.196-08:00This comment has been removed by the author.Vagstonhttp://www.blogger.com/profile/05936282034517218281noreply@blogger.comtag:blogger.com,1999:blog-6839602.post-45391046121834791832009-12-29T04:45:02.304-08:002009-12-29T04:45:02.304-08:00This comment has been removed by the author.Vagstonhttp://www.blogger.com/profile/05936282034517218281noreply@blogger.comtag:blogger.com,1999:blog-6839602.post-51505596168297916532007-08-27T12:30:00.000-07:002007-08-27T12:30:00.000-07:00Got it, thanks!Got it, thanks!Andyhttp://www.blogger.com/profile/02483089634976454808noreply@blogger.comtag:blogger.com,1999:blog-6839602.post-37206247602256282062007-08-24T13:46:00.000-07:002007-08-24T13:46:00.000-07:00You should start an architecture blog, and then I'...You should start an architecture blog, and then I'll leave the exact same comment. :-)<BR/><BR/>Anyway, here's my attempt:<BR/><BR/>"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 …"Jim Applehttp://www.blogger.com/profile/11080395413026172939noreply@blogger.comtag:blogger.com,1999:blog-6839602.post-66110159555408011942007-08-24T13:20:00.000-07:002007-08-24T13:20:00.000-07:00I don't know what that means!!No, seriously, I don...I don't know what that means!!<BR/><BR/>No, seriously, I don't know what that means. I hate my life.<BR/><BR/>Could you please write about kittens or balloons so I can read your blog?<BR/><BR/>Sincerely,<BR/>GroverAndyhttp://www.blogger.com/profile/02483089634976454808noreply@blogger.com