--- Log opened Fri Oct 01 00:00:45 2010
--- Day changed Sun Oct 03 2010
xarchhi03/10 16:08
xarchdo you know where I can find the source of “Simply Easy! An Implementation…” ?03/10 16:09
--- Day changed Tue Oct 05 2010
-!- Irssi: #epigram: Total of 13 nicks [0 ops, 0 halfops, 0 voices, 13 normal]05/10 16:37
--- Day changed Thu Oct 07 2010
realazthathey all07/10 22:23
realazthatnice language07/10 22:23
pumpkinhi :)07/10 22:27
realazthatI'm a CS newbie so maybe u guys can help me with something07/10 22:27
realazthatepigram is not turing complete correct?07/10 22:27
pumpkinI'd expect not07/10 22:29
realazthatwhat advantage does this have?07/10 22:30
realazthatfor the compiler07/10 22:30
pumpkinyou can prove anything with a program that doesn't terminate07/10 22:30
pumpkinit makes it rather difficult to trust your proofs if you're turing complete07/10 22:31
edwinbyou can optimise more aggressively too if you know things will terminate07/10 22:32
realazthatawesomeness07/10 22:32
pumpkinrealazthat: and turing completeness is overrated in practice07/10 22:32
edwinbI think a more interesting question is "what advantage does Turing Completeness give you?"07/10 22:32
realazthatepigram seems to be what im looking for07/10 22:32
realazthatedwinb: that was my next q07/10 22:32
pumpkinrealazthat: note that proofs can be monstrously difficult in general :P07/10 22:32
edwinbI asked it rhetorically ;)07/10 22:33
pumpkinI think someone showed what class of programs you could write in one of these languages07/10 22:33
pumpkinand you can definitely cover things like ackermann and such easily07/10 22:33
edwinbI've yet to find a useful program you can write in a turing complete language, but not in Epigram (or related)07/10 22:33
pumpkinso typical examples of "general recursion" can be easily expressed in simpler terms07/10 22:33
realazthatedwinb: well, an event loop would be a problem, no?07/10 22:34
pumpkinrealazthat: you can handle non-terminating but productive programs07/10 22:35
realazthatpumpkin: I agree07/10 22:35
realazthaterm07/10 22:35
realazthatpumpkin: I agree that turing completeness is overated07/10 22:35
realazthatthe language interests me in two ways07/10 22:35
edwinban event loop isn't a problem - ideally you'd like your event handlers to terminate07/10 22:35
realazthatthe expresiveness is much like math07/10 22:35
edwinbthe important thing is that you move on to the next event07/10 22:35
realazthatI really enjoyed discrete math07/10 22:36
realazthatand would love to be able to express my programs as that07/10 22:36
realazthatis epigram the right language for that?07/10 22:36
pumpkinafaik epigram doesn't have a syntax yet does it?07/10 22:36
pumpkin(2)07/10 22:37
pumpkinit does have a pig though07/10 22:37
realazthatpig is what I was looking at07/10 22:37
realazthatI didn't know there was a diff07/10 22:37
* pumpkin defers to those more knowledgeable than him07/10 22:38
edwinbwell epigram is a work in progress but it could well be the sort of language you want07/10 22:38
realazthatoops d/c07/10 22:39
realazthatand my third interest, is in a purely theoretical question07/10 22:40
realazthatis it possible to determine if a turring complete program halts (not always of course), and then take advantage of this07/10 22:41
realazthatie. automatically turn other programs into epigram if possible07/10 22:41
edwinbyou can sometimes spot that a program is going to terminate07/10 22:42
edwinbAgda does this07/10 22:42
edwinbif that's what you mean07/10 22:42
* realazthat looks up agda07/10 22:42
Saizanyou can also encode/represent non-termination explictly, so you can write programs using general recursion, and then separately prove they terminate07/10 22:43
edwinbif you know something terminates, and covers all possible inputs, you can get the same kind of optimisation advantages, same sort of guarantees that proofs are okay, and so on07/10 22:43
pumpkinrealazthat: note that it's not solving the halting problem, but rather rejecting some programs that do halt, but don't do so obviously07/10 22:43
realazthatthats exactly what I meant07/10 22:44
pumpkinthere's #agda too :) most of us are in both channels07/10 22:44
realazthatso agda *is* turing complete, but tries to compensate07/10 22:45
Saizanno, it isn't07/10 22:46
realazthatit also isn't then07/10 22:46
Saizanwell, it has flags to turn off the termination checks if you want07/10 22:46
realazthatah07/10 22:47
realazthatthats cool07/10 22:47
realazthatso it really *is*, but if it can't prove it doesn07/10 22:47
realazthat... 't halt, it will complain07/10 22:47
realazthat?07/10 22:47
pumpkinnot sure, that might be true? it explicitly prevents you from doing some things that could lead to non-termination though07/10 22:48
pumpkinbut either way, while you can write non-terminating programs, non-productive in agda, you basically lose any advantages agda gives you by doing so07/10 22:49
pumpkinew, that sentence got mangled by a bad edit :P07/10 22:50
realazthatso aside from a language, epigram is also a prover?07/10 22:50
realazthathow does it relate exactly07/10 22:50
pumpkinhttp://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence07/10 22:50
realazthat(I've recently also become very interested in provers as well)07/10 22:51
pumpkinwhy is there an en-dash in that page name?07/10 22:51
realazthathttp://en.wikipedia.org/wiki/Talk:Curry%E2%80%93Howard_correspondence#Article_name07/10 22:53
realazthatlol07/10 22:53
realazthatinteresting07/10 22:55
realazthatits funny, I've been doing a lot of research in a few areas recently and its all coming together07/10 22:56
realazthathmm07/10 23:01
realazthatis it possible to compute the computational complexity of a function then?07/10 23:01
edwinbI have wondered about this sort of thing07/10 23:03
edwinbI could imagine you could impleement a language which made the complexity explicit in the type07/10 23:03
edwinbNils Anders Danielsson has done something along those lines07/10 23:03
* realazthat googles07/10 23:04
pumpkinit'd probably be easier to do if you write your algorithms explicitly in terms of all those crazy recursion schemes07/10 23:04
edwinbwhen I tried to do it the difficulty was recursion, yes07/10 23:04
edwinbI decided my the complexity of my time should be less.07/10 23:04
edwinbso did something else instead07/10 23:05
realazthatlol07/10 23:05
realazthatI have another fuzzy idea07/10 23:07
realazthatare you familiar with LLVM?07/10 23:07
realazthatits basically a virtual assembly which has many frontend languages07/10 23:10
realazthatand many backend languages as well07/10 23:10
edwinbI haven't spent nearly enough time looking at LLVM07/10 23:11
edwinbI'd quite like to try it as a backend for epigram07/10 23:11
realazthathmm07/10 23:11
edwinbbut it needs a front end first :)07/10 23:11
realazthat;)07/10 23:11
edwinbit seems it might be a good fit07/10 23:11
realazthatI might be able to help some07/10 23:11
edwinbwith llvm?07/10 23:11
realazthatI've dabbled a few times with it b4, nothing serious07/10 23:11
realazthatyeah07/10 23:11
realazthatits very well documented07/10 23:12
edwinbI have a small functional language to be used as a back end, Epic07/10 23:12
edwinbhttp://www.cs.st-andrews.ac.uk/~eb/epic.php07/10 23:12
edwinbCurrently it compiles to C07/10 23:12
edwinbbut I'd quite like to try LLVM07/10 23:12
realazthatit should be straightforward07/10 23:13
edwinbI think so07/10 23:14
edwinbthe tricky bit, if it is to be done well, would be integrating a garbage collector07/10 23:14
realazthatbasically, what I want to do, is lower the advantages of epigram to the LLVM IR level07/10 23:14
realazthatthe advantages being the turing incompleteness07/10 23:15
realazthatthere is a project called KLEE07/10 23:15
realazthatsister to LLVM07/10 23:15
realazthatwhat it does is it uses an SMT solver07/10 23:15
realazthatand trys to find bugs07/10 23:16
realazthatand produce counter examples to defined behavior07/10 23:16
edwinboh, I don't know that one07/10 23:16
realazthatthe way KLEE works gave me an idea07/10 23:16
pumpkinyep, was just looking at KLEE yesterday actually07/10 23:17
realazthatcool ;)07/10 23:17
realazthatit gave me an idea to verify that a program will not assert07/10 23:17
realazthatusing an SMT solver07/10 23:18
realazthatthus, specifications can be written in terms of assertions07/10 23:18
pumpkinthere's only so much you can do with SMT though :P07/10 23:18
realazthatyeah07/10 23:18
realazthatnow I'm a newbie to provers, SMT, CS etc.07/10 23:19
realazthatso I'm not 100% clear on the limitations07/10 23:19
realazthatbut my idea is more extensive than that07/10 23:19
realazthatand I suspect I will have to use provers and smt07/10 23:19
realazthatI'm writing up a wiki page07/10 23:20
pumpkinactually writing proofs is the hard bit :)07/10 23:20
realazthaton the features I would like to see07/10 23:20
pumpkinstating properties is comparatively easy07/10 23:20
realazthatI meant automated provers07/10 23:20
edwinbwritings proofs is tedious and the more we can get the machine to do by magic the better07/10 23:21
edwinbapart from anything else, programmers are lazy and would like the machine to say, "yes", or "no, because ..." rather than "go on, prove it"07/10 23:21
edwinbI claim07/10 23:21
pumpkinI agree :)07/10 23:22
realazthatlol i agree07/10 23:22
edwinbalthough I find a lot of the proofs I do are really boring and obvious things like list membership, or slight modifications of things in the context07/10 23:22
edwinbI have some hope that these can be automated most of the time07/10 23:22
realazthatheh, i'm no expert mathametician either07/10 23:22
realazthatI'm an ameteur all around guy07/10 23:23
realazthatI just see a way to bring lots of tools together07/10 23:23
realazthatand solve all the worlds problems07/10 23:23
realazthatheres what I have so far07/10 23:27
realazthathttp://realazthat.wikkii.com/wiki/LLVM/Formal_methods07/10 23:27
realazthatI'm curious about how much of that is theoretically possible07/10 23:28
edwinbI've no idea to be honest ;)07/10 23:32
edwinbhave you seen Typed Assembly Language and related stuff?07/10 23:32
edwinbDependently Typed Assembly Language, Proof Carrying Code, etc07/10 23:32
realazthatno07/10 23:33
* realazthat googles07/10 23:33
edwinbdoesn't go as far as you're suggesting, but might be a starting point07/10 23:33
edwinband give some ideas about how plausible it might be07/10 23:33
realazthatvery cool07/10 23:35
realazthatproof-carrying code is a very nice concept07/10 23:37
edwinbI haven't seen much work on it lately though07/10 23:38
realazthatI've seen similar ideas, minus the proofs07/10 23:39
realazthatgoogle's native client07/10 23:39
realazthatsimilar to Tal07/10 23:39
realazthatit would filter bad instructions out07/10 23:39
realazthatI think they switched to using LLVM though07/10 23:39
realazthathttp://llvm.org/pubs/2007-SOSP-SVA.pdf07/10 23:45
realazthatsimilar to Tal86, comparison at the end07/10 23:46
realazthatanother CS question07/10 23:46
realazthatis it possible to prove equivelence of two functions in epigram?07/10 23:47
Saizanyes07/10 23:48
realazthatcool07/10 23:48
realazthathmm07/10 23:48
realazthatthat can be used to help prove a spec07/10 23:48
realazthatno?07/10 23:49
Saizanthe general way is to prove that for all the inputs they will return the same output07/10 23:49
Saizanin the sense that you might have a reference implementation and you want to prove your real one is equivalent?07/10 23:49
Saizansure07/10 23:50
realazthatdisconnected07/10 23:50
realazthatwould that not take forever?07/10 23:51
pumpkinyou'd hope not07/10 23:52
Saizaninduction should spare you from doing an exhaustive check :)07/10 23:54
realazthat;)07/10 23:56
realazthatgood point07/10 23:56
* realazthat remembers induction from discrete07/10 23:56
realazthatcan induction always be done?07/10 23:57
realazthathmm07/10 23:57
pumpkinif not induction, then coinduction!07/10 23:57
Saizanbtw, via Curry-Howard induction is really the same thing as writing a function by recursion on the structure of its argument07/10 23:58
--- Day changed Fri Oct 08 2010
realazthatare there any other interesting properties that can be determined from a non-Turing-complete program?08/10 00:05
dolioedwinb: What about an epigram interpreter? :)08/10 01:22
dolioOr are those not useful? :)08/10 01:23
edwinbhave you tried running one? ;)08/10 01:23
merijnAny recommendations for a good introductory paper on Epigram? Or should I just pick any of the papers mentioned on lambda-the-ultimate at random?08/10 22:47
Saizanthere's a ltu thread about Epigram 2?08/10 22:51
merijnNot sure if there's one on Epigram2, but plenty related to Epigram08/10 22:51
Saizani'd probably go with "Observational Equality, Now!" "The Gentle Art of Levitation", and the blog08/10 22:54
merijnI'll check those out, thanks08/10 22:58
Saizan..though i don't think i understand the latter part of the former08/10 23:00
merijnBy now I've gotten used to reading papers I only understand for like 25% :p08/10 23:02
ccasinSaizan: but you do understand all of Levitation?08/10 23:25
ccasinseems like no small feat :)08/10 23:27
Saizanccasin: let's say that in that case i'm not aware of what i don't understand :)08/10 23:29
--- Day changed Sat Oct 09 2010
dolioQuite a few of the epigram 1 papers are excellent, too.09/10 01:31
dolioWhy Dependent Types Matter, for instance.09/10 01:31
--- Day changed Mon Oct 11 2010
Saizanhas anyone considered porting the levitation concept at the value level?11/10 16:33
agundrySaizan: what do you mean?11/10 16:39
Saizanagundry: IDesc reifies the definition of types, something else could reify the definition of functions over those types11/10 16:56
Saizanin fact IDesc would be a special case of the latter, since it's really a syntax for strictly positive functions of type (I -> Set) -> (I -> Set)11/10 16:58
--- Day changed Tue Oct 12 2010
stevanSaizan: wasn't something like that mentioned as a loose end in the ornaments post?12/10 00:02
Saizanstevan: you refer to the comment about deriving (++) from (+)?12/10 00:04
stevanyea12/10 00:05
Saizanmh, maybe, it was quite vague12/10 00:07
Saizanah, less then i remembered12/10 00:10
Saizanbut my point above was to have such an universe as the base of your language12/10 00:11
--- Day changed Wed Oct 13 2010
realazthathmm13/10 02:03
realazthatI wish there was an epigram interpreter online13/10 02:04
realazthatoy, I'm running into trouble install she13/10 15:56
realazthatCompiling ShePrelude ... panic! the impossible happened13/10 15:56
realazthatNon-exhaustive patterns in function choose_univs ...13/10 15:57
agundryrealazthat: which GHC version are you using?13/10 15:59
realazthat6.8.213/10 15:59
realazthatx86_64-unknown-linux13/10 15:59
agundryI think she requires at least 6.10, and maybe even 6.12 now13/10 15:59
realazthatah13/10 15:59
realazthathmm13/10 16:00
realazthatapt-get got me that13/10 16:00
agundryshe makes extensive use of type-level hackery that was only recently introduced13/10 16:00
realazthathow do I get the latest ghc13/10 16:00
agundryI usually just download the binaries (http://www.haskell.org/ghc/download_ghc_6_12_3.html)13/10 16:03
agundrythere's also the Haskell Platform (http://hackage.haskell.org/platform/linux.html) but I've never tried using it13/10 16:04
realazthatcool i'll do that13/10 16:05
agundrygood luck13/10 16:07
xrchhi13/10 16:33
realazthathi13/10 17:04
--- Day changed Mon Oct 18 2010
realazthathey all18/10 19:27
Saizanhi18/10 22:26
pumpkinhi!18/10 22:27
realazthatheres a CS question18/10 22:27
realazthatdo you know of any compiler optimizations/algorithm tranforms etc. that change the complexity of a function18/10 22:28
dolioYes.18/10 22:29
doliofoldl' (\e r -> r + e/sum l) 0 l -- O(n^2)18/10 22:32
doliolet s = sum l in foldl' (\e r -> r + e/s) 0 l -- O(n)18/10 22:32
dolioWhich you can probably call... constant floating. Or something like that.18/10 22:33
realazthathmm18/10 22:38
realazthatisn't constant-folding like dead code elimination?18/10 22:39
dolioConstant folding is like compile-time partial evaluation.18/10 22:46
dolioWhere you turn "10 * 30" into "300".18/10 22:46
dolioBut I said floating.18/10 22:46
dolioWhere you lift some constant out of a lambda/local function/whatever to avoid recomputation.18/10 22:47
dolioThat is, a constant expression.18/10 22:48
dolio\<v> -> ... e ... => let s = e in \<v> -> ... s ...18/10 22:49
realazthatright18/10 22:51
realazthatand then something like a loop or recursion can be eliminated18/10 22:51
realazthatresulting in a complexity change18/10 22:51
realazthatie. dead code elimination18/10 22:51
dolioWell, you do the loop once, instead of redoing it in every iteration of a second loop.18/10 22:52
realazthatah18/10 22:52
realazthatthat too18/10 22:52
realazthatI'm trying to find all the methods of algorithm transformation18/10 22:53
dolioAnyhow, that can change something like O(m*n) into O(m + n), or similar.18/10 22:53
realazthatie. compiler optimizations etc.18/10 22:53
realazthatthat change complexity18/10 22:53
realazthathttp://rosettacode.org/wiki/User:Realazthat/Projects_wishlist/LLVM/Strategic_optimizations18/10 22:53
realazthatI'm curious if there is anything special about a decidable language (like epigram) that allows for uncovering new algorithms18/10 22:54
dolioA more ambitious version of that would be some kind of memoization.18/10 22:54
realazthator tail call optimizations18/10 22:54
realazthatfor space complexity18/10 22:55
dolioBut achieving memoization merely by transforming code isn't something I'd expect to be easy.18/10 22:55
realazthathmm18/10 22:55
realazthatI don't see why not18/10 22:55
realazthatits more of a question of when to do it18/10 22:55
dolioI think there are experiments in graph rewriting that, say, try to turn a naive fibonacci function into an efficient one, though.18/10 22:55
realazthatthats what I'm looking for18/10 22:56
realazthatlinkme?18/10 22:56
dolioI don't have links. Just something I recall hearing about in the murky past.18/10 22:56
realazthatheh18/10 22:56
Saizanrealazthat: edwin brady thesis has a few opimizations that exploit the strong normalization property18/10 22:56
realazthati've been googling different combinations of keywords trying to find something like this all week18/10 22:56
dolioLook for "term graph rewriting," though.18/10 22:57
Saizanand can change asymptotics too18/10 22:57
Saizanhttp://www.cs.st-andrews.ac.uk/~eb/writings/thesis.ps.gz18/10 22:57
Saizanor look for thesis here http://www.cs.st-andrews.ac.uk/~eb/18/10 22:58
realazthatty for all the pointers ;)18/10 23:00
--- Log closed Tue Oct 19 10:49:34 2010
--- Log opened Tue Oct 19 10:49:41 2010
-!- Irssi: #epigram: Total of 13 nicks [0 ops, 0 halfops, 0 voices, 13 normal]19/10 10:49
-!- Irssi: Join to #epigram was synced in 93 secs19/10 10:51
--- Day changed Wed Oct 20 2010
merijnSo I'm reading "The view from the left" and it seem to expand on Luo's UTT, anyone aware of any quick crash courses on that? The only thing I can find is the cited book by Luo which I can't easily get at the moment.20/10 20:37
roconnormerijn: I didn't know UTT when I read that paper20/10 20:44
merijnroconnor: Depends on how at home you are in type theory I guess? The figure 1 illustrating the UTT syntax is just to dense for me to grok20/10 20:45
merijnI've crammed the entire basics of type theory in my head in like 2-3 weeks, a sparse figure illustrating a dependently typed syntax isn't going to cut it...20/10 20:46
ccasinmerijn: I don't know of any really excellent intro to all of UTT (maybe luo's book is the best).  But, Ulf Norell's thesis begins with an introduction to most of UTT20/10 21:00
ccasinThe trickiest part is the data types, and as far as I know no good introduction to those exists.  But, at least in Ulf's thesis they are separated out a bit20/10 21:01
ccasinYou might also look at some of the introductory material for coq.  UTT is very close to CC + datatypes + universes20/10 21:02
ccasinYes, in fact, that's probably your best bet - writing a few coq or agda programs will get you going in the syntax and then you'll find the view from the left much easier20/10 21:04
ccasinmaybe one of the agda tutorials is best, since they are focused on programming20/10 21:04
merijnReading this paper is turning into yak shaving >.>20/10 21:15
doliomerijn: You can read Luo's thesis on ECC. It's pretty similar to UTT, and freely available.20/10 21:18
dolioAnd I don't think view from the left makes use of the significant differences.20/10 21:18
merijndolio: Ok, I'll look it up, thanks20/10 21:19
dolioWell, I guess it probably makes use of datatypes, but I don't think Luo's UTT stuff is very good for learning about those anyway.20/10 21:21
--- Day changed Wed Oct 27 2010
shaprpigworker: You planning on being in north america anytime soon?27/10 17:24
pigworkershapr: not that I'm aware of, but it does seem to happen quite often27/10 17:25
shaprheh, ok then27/10 17:25
pigworkerIt's possible I might acquire reasons to go to POPL, but I don't have any papers at that meeting.27/10 17:27
shaprWell, if you do show up in north america, I've heard that buying you drinks is a great way to learn stuff and have fun.27/10 17:27
pigworkershapr: I'm never sure whether this is a good reputation or a bad one...27/10 17:28
shaprWell, it's not boring... so that's positive, yah?27/10 17:29
edwinball the best work happens in the pub27/10 17:29
pigworkerI guess. I'd far rather be interesting than right.27/10 17:29
--- Day changed Fri Oct 29 2010
copumpkin_has there been much thought on the notion of a generic "index" into a data structure, like a zipper is a cursor for a structure?29/10 03:29
copumpkin_Nat is a natural index into List and Fin n is natural into Vec n (these could probably be unified somehow with the ornaments stuff?)29/10 03:31
copumpkin_if you had a binary tree you could imagine a list of bools as an index into it, though29/10 03:32
Saizani think one can define a generic `elem` type through zippers, and Nat is just `elem` for list after you've erased the indices29/10 03:34
copumpkin_hmm29/10 03:35
copumpkin_how about more complicated types though?29/10 03:35
copumpkin_say you have a data Moo b a = X a | Y (b -> Moo b a) = Free (b ->) a29/10 03:36
copumpkin_a b-branching tree of a elements unless I screwed up29/10 03:36
SaizanM' a = 1 + b*(M a)^(b-1)*M' a -- so it tells you what 'b's to use to get to the right branch, the (M a)^(b-1) term is just there to store the other branches, which would be needed to restore the original list which would appear in the index29/10 03:46
Saizans/index/index of elem/29/10 03:46
* Saizan wonders if there's an easy way to spot the terms you can discard29/10 03:48
Saizanmaybe we can just substitute occurrences of the original type with \top29/10 03:50
copumpkin_also, is there an equivalent "safe-indexing" tree structure to Vec + Fin ? :P29/10 03:51
copumpkin_anyway, gotta run, will check logs29/10 03:51
Saizansince \top^(b-1) = \top29/10 03:51
SaizanNat ~ List \top: i.e. you discard the elements and keep only the structure29/10 04:01
Saizanthrough this glass you have: Fin xs ~ _ `elem` xs29/10 04:03
dolioNat is not a natural index into List.29/10 04:08
dolioIt's an index for streams.29/10 04:08
Saizanyeah, it's not "bounded" by the shape of the list like Fin instead is29/10 04:09
dolioYou can see this because Vec A n ≅ Fin n → A, and Stream A ≅ ℕ → A29/10 04:09
dolioList A = Σ[ n : ℕ ] (Fin n → A)29/10 04:10
dolioColist A ≅ Σ[ n : ℕ̃ ] (∣ n ∣ → A)29/10 04:14
dolio∣ n ∣ being the set of size n.29/10 04:14
Saizanhow does that differ from Fin n?29/10 04:15
dolioℕ̃ is the coinductively defined extended natural numbers.29/10 04:16
dolioSo there's an infinite value, and the set with that size is the natural numbers.29/10 04:16
Saizanah, the squiggle above the N is too small here :)29/10 04:17
dolioAm I mistaken in thinking that for f, g : Z -> 0, where 0 is an initial object, f = g?29/10 04:21
dolioIt seems like it should hold, but I've been failing to prove it for a while now.29/10 04:21
dolioAnd I tried coming up with counter examples, but failed at that, too.29/10 04:22
Saizanif you have h : Z -> 0, shouldn't you be able to demonstrate that Z is isomorphic to 0? so f and g can only be id_0 ?29/10 04:28
dolioI thought so, but how?29/10 04:28
Saizanno, wait, for monoids the initial object is also terminal, but the category of monoids has more than one object29/10 04:32
dolioOkay.29/10 04:33
dolioThat doesn't necessarily invalidate my conjecture, though.29/10 04:33
Saizanyeah29/10 04:33
dolioEquivalently, is ! : 0 -> 1 monic?29/10 04:37
dolio0 initial, 1 terminal.29/10 04:37
dolioI guess the answer to that is "no."29/10 04:40
dolioOr is it?29/10 04:41
dolioNo, I can't say for certain that's false, either.29/10 04:43
dolioI was thinking you could have, for instance, f, g : R -> ℤ, f /= g, but ! . f = ! . g, but I don't think that's true.29/10 04:45
Saizanwhich category is that?29/10 04:46
dolioOh, sorry. Category of rings.29/10 04:46
dolioOr is it possible? Maybe R = Z[x]?29/10 04:48
doliof x -> 0, g x -> 1.29/10 04:50
dolioI'm not sure ! monic is equivalent to what I want, but it's sufficient.29/10 04:50
Saizanmy ring-fu is weak, but R = the Reals, f = floor; g = ceiling ?29/10 04:51
dolioHmm...29/10 04:52
dolioI'm not sure those are homomorphisms.29/10 04:52
Saizanme neither.29/10 04:52
doliofloor (-3.5) = -4, - (floor 3.5) = -3.29/10 04:53
dolioI think polynomials with integer coefficients work, though.29/10 04:54
dolioYou can send the variable to any value of your choice.29/10 04:54
dolioYou could also use round-away-from-0 and round-toward-zero instead of floor and ceiling, I think.29/10 04:57
* dolio hits the hay.29/10 04:58
pigworkercopumpkin: "index into" is logarithm the way "context" is derivative; this is what the container-theory stuff deals with29/10 14:13
pigworkerHancock to McBride, many years ago, "Now, you be Leibniz and I'll be Napier..."29/10 14:14
copumpki_pigworker: oh, thanks! I haven't come across that one29/10 15:31
copumpki_pigworker: do you have a citation or paper title to point me at for the container logarithm stuff?29/10 15:32
pigworkercopumpkin: there's some work by Ralf Hinze and other work by Thorsten Altenkirch on memoization which explains exponentiation (memoize a Nat -> X as a Stream X), but the log view never quite appeared so explicitly29/10 17:12
pigworkermeanwhile, the Container literature (Altenkirch, Ghani, various others) is all about giving a general shape-and-position analysis of structures with elements in29/10 17:14
pigworkerI woke up one morning on someone else's sofa, realising that if F X = 1, then log F = dF 1.29/10 17:16
pigworkerThat is, if there's no choice of F-shape, then an F-position is a one-hole F-context with its elements erased.29/10 17:18
* dolio doesn't follow.29/10 17:22
pigworkeroops; I meant if F 1 = 1, then log F = d F 129/10 17:22
pigworkerBy log F, I mean log-to-the-base-X of F X.29/10 17:23
pigworkerso that  F X ~= (log F) -> X29/10 17:24
dolioYeah. Okay, I believe that second one, I guess.29/10 17:24
pigworkerso the law d (F * G) = d F * G + F * d G   gives you  log (F * G) = log F + log G  in that case29/10 17:27
pigworkerI'm not sure if or why it makes much sense in real analysis, but it makes a lot of sense for containers.29/10 17:40
dolioThe connection seems non-obvious.29/10 17:47
dolioYou don't really take logs of functions to get numbers.29/10 17:47
* shapr logs the function29/10 19:22
--- Day changed Sat Oct 30 2010
dolioSaizan: So, I came up with another example to confirm the initial object thing. That puts a nail in the coffin, I guess.30/10 01:10
dolioI had been trying to come up with F-algebra counterexamples, but didn't pick the right one.30/10 01:10
dolioBut, Nat + Nat is a natural number algebra, and it has infinitely many different homomorphisms into Nat.30/10 01:11
Saizandolio: because one of the two zeros can be mapped anywhere?30/10 01:17
dolioRight.30/10 01:17
Saizannow we can ask when is it the case that all the arrows into the initial object are equal :)30/10 01:19
dolioYeah. Well, the reason I was even thinking about this, was that I wanted a categorical argument that if you have P <-> ~~P, then all propositions are trivial in structure.30/10 01:21
dolioAnd that led me to think about the homset A -> 0. But that isn't always trivial.30/10 01:22
Saizanby trivial you mean that there's at most one value inhabiting P? 30/10 01:28
dolioYes.30/10 01:28
dolioAnyhow, obviously I need to make more reference to the structure of categories that model logic. But I'm not totally sure what.30/10 01:29
Saizani've seen the term "double negation stable" before, but google only finds a paper on ultrasheaves(?)30/10 01:30
SaizanWe say a proposition φ is decidable if φ + ¬φ holds. Every decidable proposition is stable.30/10 01:34
Saizanfrom http://www.citeulike.org/user/pedagand/article/761885630/10 01:35
Saizanand i guess it's easy to come up with a decidable proposition that isn't trivial?30/10 01:35
dolioIt might depend on what you expect of the biimplication.30/10 01:39
dolioIf P is supposed to be isomorphic to ~~P, I'd expect such P to be trivial.30/10 01:40
dolioYou can have decidable, nontrivial constructive propositions, but they wouldn't be isomorphic to their double negation, I think.30/10 01:41
Saizanah, ok, i wasn't thinking of isomorphisms, just propositional equivalence30/10 01:49
dolioI'm almost certain I've heard that categories that include some form of excluded middle require such triviality, so maybe there's something that requires it to be an isomorphism.30/10 01:51
dolioI could be mistaken, too, of course.30/10 01:52

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