--- Day changed Mon Jul 03 2017
fsestinihello. i was wondering… is it possible to derive eta-equality or function extensionality in extensional type theory with elimination rule of Pi type formulated as application, and without assuming eta as a rule of the type?03/07 13:27
fsestinimy guess is it can’t be done, but I couldn’t find proofs of it in the literature, except maybe Garner’s paper on dependent product03/07 13:28
Saizanfsestini: so you only have a congruence rule for lambda in the judgmental equality?03/07 13:41
fsestiniSaizan: yes03/07 13:41
fsestiniand the “extensional” is only given by the addition of equality reflection and UIP03/07 13:41
Saizani guess you can only prove ((x : A) -> f x = g x) -> (\x -> f x) = (\x -> g x)03/07 13:42
fsestinii agree03/07 13:49
TanebHow dangerous is postulating extensionality?03/07 21:04
comietekTaneb: https://en.m.wikipedia.org/wiki/Bogosort03/07 21:07
Tanebcomietek, that's a really useless answer to my already rather useless question03/07 21:08
comietekwell, I'm sad you think so03/07 21:08
comietekI actually think is a really good answer03/07 21:09
comietekif you postulate extensionality, you are saying you don't care whether your sorting function manages to sort things before the heat death of the universe03/07 21:09
TanebCan you explain that?03/07 21:10
comietekwhat is unclear?03/07 21:10
TanebWhere your conclusion comes from03/07 21:11
comietekfunction extensionality means that any two functions of the same type are equivalent03/07 21:12
comietekbut unless you account for every possible observable effect in the type, including running time03/07 21:12
TanebI don't see how03/07 21:12
comietekuh.03/07 21:13
comietekcan you state the proposition you would postulate?03/07 21:13
Tanebhttp://agda.github.io/agda-stdlib/Relation.Binary.PropositionalEquality.html#632403/07 21:13
comietekthat's not stating it03/07 21:14
comietekcan you use your own words to state it?03/07 21:14
akr[m]if two functions behave the same on all inputs, then they are in fact the same03/07 21:15
TanebWhat akr[m] said03/07 21:15
comietekso…?03/07 21:15
comietekbogosort behaves as quicksort on all inputs03/07 21:16
comietekdo you think bogosort is the same as quicksort?03/07 21:16
TanebIt's the same function03/07 21:16
TanebBut a different algorithm, which I don't care about03/07 21:16
comietekI rest my case03/07 21:16
comietekif you don't care about that, then you don't have anything to worry about03/07 21:17
akr[m]> comietek, that's a really useless answer to my already rather useless question03/07 21:17
lambdabot <hint>:1:9: error: parse error on input ‘,’03/07 21:17
comietekmy position is that not caring about that is dangerous in itself03/07 21:17
akr[m]what was this a reply to? (sorry, I don't see it)03/07 21:17
Taneb<Taneb> How dangerous is postulating extensionality?03/07 21:17
comietekakr[m]: link to Wikipedia on Bogosort03/07 21:17
comietekTaneb: have I managed to explain sufficiently well now?03/07 21:20
Tanebcomietek, eventually03/07 21:21
TanebThere would have been better starts to the explanation than linking a seemingly unrelated wikipedia article without explanation though03/07 21:21
comietekplease check your entitlement03/07 21:21
Nik05mietek, I also watched Pfennings lecture from 2015, have the feeling I understand that a little better03/07 23:16
Nik05He also did some small temporal logic with just one introduction and elimination rule. But how would you implement something like that in Agda?03/07 23:17

Generated by irclog2html.py 2.7 by Marius Gedminas - find it at mg.pov.lt!