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 
inte 
Pierce's law is classical, but how about Eps (%x.False) ;) 
15:13 
inte 
Peirce even. 
15:21 
inte 
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:24 
pruvisto 
funnily enough, larsrh talked about this a few days ago as well 
15:26 
inte 
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 
inte 
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 
inte 
chuchucorny: the version of the curryhoward 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 
inte 
s/realizable/inhabited/ 
17:49 
JCaesar 
Uh. Is Pierce's law provable in in intoitionistic propositional logic? (damnit, I should know that…) 
17:51 
inte 
no it's not. 
17:53 
inte 
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 
inte 
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 
inte 
can you give those sane names using `lemmas`? 
18:39 
inte 
(though I guess what you really need is an alias for a namespace... :/) 
18:44 

ammbauer joined #isabelle 