# IRC log for #isabelle, 2017-01-27

All times shown according to UTC.

Time Nick Message
06:59 larsrh joined #isabelle
12:05 JCaesar pruvisto: Psst. You're not supposed to talk about the elephant in the room.
12:13 pruvisto JCaesar: you mean the three elephants in the room
12:22 silver joined #isabelle
14:46 chuchucorny Is there a definition of a function (not using undefined) which hast the type signature (('a => 'b) => 'a) = 'a?
15:05 JCaesar if you want (('a => 'b) => 'a) => 'a, then why not use f a b = b?
15:05 JCaesar oh, wait…
15:07 JCaesar mh… am I getting this right now? You're asking whether it's possible to define a function 'a => 'b without undefined?
15:13 int-e Pierce's law is classical, but how about  Eps (%x.False) ;-)
15:13 int-e Peirce even.
15:21 int-e chuchucorny: an interesting implemetnation in a functionla programming language with exceptions is something like   \f -> try (f (\x -> throw (Result x))) catch Result x -> x
15:26 int-e I hope he had fewer typos.
15:35 larsrh it is morally dubious though (at best)
15:36 larsrh at worst it is an attack on sound reasoning
15:37 int-e I admit that I sometimes have impure thoughts.
17:24 chuchucorny I thoght due to the curry howard isomorphism it should be possible to have such a function in Isabelle? What did I not understand? Does it just mean there is such a function for specific types, e.g., it is easy if I take "nat" instead of "'b"? Do I need to use things such as undefined, e.g., "foo f = f (\<lambda>x. undefined f x)"?
17:28 int-e chuchucorny: the version of the curry-howard isomorphism I had in mind is that a type built from variables and => is realizable in the simply typed lambda calculus iff it is provable in intuitionistic propositional logic. Note the "intuitionistic".
17:29 int-e s/realizable/inhabited/
17:49 JCaesar Uh. Is Pierce's law provable in in intoitionistic propositional logic? (damnit, I should know that…)
17:51 int-e no it's not.
17:53 int-e you an use it to establish double negation elimination: If (a -> _|_) -> _|_ then (a -> _|_) -> a (_|_ -> a holds by absurdity), and using Peirce's law, that implies a.
17:56 int-e also, /msg lambdabot @djinn ((a -> b) -> a) -> a   will tell you that the type is not realizable... if you trust it :)
18:09 larsrh apply (rule rules_as_nrules.crules_as_irules'.irules'_as_prules.prules_as_srules.srewrite_wellformed_rt)
18:09 larsrh this is not going to end well
18:37 int-e can you give those sane names using `lemmas`?
18:39 int-e (though I guess what you really need is an alias for a namespace... :-/)
18:44 ammbauer joined #isabelle