←2014-12-21 2014-12-22 2014-12-23→ ↑2014 ↑all
00:03:34 -!- |oren\ has joined.
00:03:58 <|oren\> i am back online
00:04:05 <vanila> you were needed
00:04:50 * |oren\ reads the logs...
00:06:40 <|oren\> noise sensitivity eh. i have the opposite problem, i can't fall asleep in the country because it is too quiet and i need the sound of the city to put me to sleep
00:06:47 <oerjan> <|oren\> when goto is used wisely it pervents confusion <-- i think "pervent" is the perfect word for what happens if you try to use goto wisely
00:09:23 <|oren\> goto is actually a less confusing construct today because of the existence of editors that can search for the label.
00:10:30 <oerjan> OKAY
00:10:33 <|oren\> (less confusing as compared to adding a new boolean variable)
00:11:14 <oerjan> i also think adding a new boolean variable may mean you've missed the point of avoiding goto
00:11:24 <|oren\> it pervents more confusion than it causes
00:11:47 <oerjan> (psst you did realize i was teasing about the misspelling, right?)
00:12:12 <|oren\> well from now on i'm spelling it like that every time. like biguate.
00:12:30 -!- oerjan has set topic: Mandatory spelling lessons in 1,2... | https://dl.dropboxusercontent.com/u/2023808/wisdom.pdf http://codu.org/logs/_esoteric/ http://tunes.org/~nef/logs/esoteric/.
00:13:03 <Jafet> Shouldn't it be mbiguity
00:13:35 <|oren\> ambiguity->antonym = biguity
00:14:10 <oerjan> am- as a negative prefix almost makes sense but not quite.
00:14:18 <|oren\> but to be fair in modern greek the sound b is written mu beta
00:14:27 <oerjan> huh
00:14:45 <oerjan> oh because beta is a fricative
00:14:52 <|oren\> yeah
00:15:10 <Phantom_Hoover> surely it's ambiguity, as opposed to chiral guity?
00:15:30 <oerjan> wat
00:15:36 <oerjan> oh hm
00:15:43 <|oren\> guities can be bi, or ambi.
00:16:06 <oerjan> dextroguity
00:16:08 <elliott> bisexual guity
00:16:24 <oerjan> (that -o- has to be wrong)
00:16:25 <myndzi> |
00:16:25 <myndzi> /<
00:16:32 <oerjan> thanks myndzi
00:16:51 <|oren\> oh man XD
00:19:03 <oerjan> if ambisexual means something different from bisexual than YOU GO TOO FAR
00:19:26 <oerjan> YOU AM PLAY GODS
00:20:13 <Phantom_Hoover> i think CPT symmetry means you're having reverse sex with your antimatter twin?
00:21:09 <oerjan> that sounds hot. explosive, even.
00:23:30 <Solace> Bi means you like male and female
00:23:38 <Solace> Ambi means you like chairs?
00:23:45 <Solace> Thats all ive gotten
00:24:06 <oerjan> i don't know that ambi- has anything to do with chairs
00:24:20 <Solace> Idk either
00:24:28 <Solace> Guys
00:24:33 <oerjan> it's the latin word for "both"
00:24:50 <elliott> I like chairs.
00:24:53 <|oren\> Solace: yeah what?
00:24:54 <Solace> Semen has clocked in the scale for best cpu coolant next to artic silver
00:25:02 <Solace> Just saying
00:25:06 <|oren\> bullshit
00:25:32 <oerjan> [citation ne...NO NO NO]
00:26:02 <oerjan> also what is artic silver
00:26:28 <Jafet> [unreliable source?]
00:29:21 <elliott> just gotta jizz all over my CPU to test
00:29:24 <elliott> "brb"
00:31:45 <Solace> Lol
00:31:57 <Solace> Probably Jafet
00:32:19 <Solace> I was just skimming a forum and thats all i saw
00:32:24 <Solace> You never know
00:32:42 <Solace> Maybe thermite and blood makes a great coolant
00:32:58 <oerjan> forums are not reliable sources: world scientific community shocked
00:33:07 <Solace> ^
00:33:30 <oerjan> *-are
00:33:36 <Solace> Topic is set to that why?
00:33:48 <oerjan> because y'all need to learn to spell hth
00:34:10 <Solace> Eye sea watt yew did their oerjan
00:34:18 <Solace> hth
00:34:45 <Solace> Jk so like what is brainfuck and why does it look like garbage and syntax
00:35:15 -!- nyuszika7h has quit (Ping timeout: 258 seconds).
00:35:33 <oerjan> it was designed to have a very small compiler which means it needs to be extremely simple
00:35:37 -!- nyuszika7h_ has joined.
00:35:49 <Solace> :0
00:36:04 <Solace> So is it hard?
00:36:18 <oerjan> (unlike most other esolangs which look like garbage because most esolangers don't bother to invent parsing)
00:36:49 <Solace> The way you phrased that made me laugh
00:37:04 <vanila> Its hard to use BRINAFUKK
00:37:12 <vanila> beacuse it doesn't have procedures
00:37:21 <oerjan> ok some look like garbage because they're inspired by the others that do
00:37:31 <Solace> Ah
00:37:35 <vanila> or GOTO
00:38:05 <oerjan> (most commonly, brainfuck)
00:40:02 <myname> brainfuck looks like garbage? it's perfectly readable to me
00:41:00 <shachaf> `pbflistdeluxe
00:41:01 <HackEgo> pbflistdeluxe:
00:41:12 <oerjan> brainfuck is hard because it's so low level that you have to implement almost everything from scratch, including any advanced data structures - you don't even have pointers or references.
00:41:36 <oerjan> and also because it has no real form of abstraction
00:43:39 <Solace> Thats horrifying
00:43:45 -!- yorick has quit (Read error: Connection reset by peer).
00:44:02 <Solace> I will never try my hand at that ._.
00:44:03 <oerjan> well that means it's more of a puzzle than actually useful
00:44:08 <elliott> vanila: is BRINAFUKK a bf derivative
00:44:32 <vanila> BRINAFUKK Is Not A BRINAFUKK Derivative
00:44:41 <oerjan> Solace: _many_ esolangs share those "features"
00:44:51 <Solace> Well
00:45:03 <myname> Solace: are you sure you are at the right place?
00:45:05 <Solace> Ill only use esolangs that have letters
00:45:26 <Solace> >+] is to much for me
00:45:50 <Solace> myname: yeh i am im usually afk doing stuff though
00:46:05 <myname> Solace: so a substitution of +-<>.,[] with idbfpcse is fine?
00:46:07 <elliott> vanila: BINABD. yep, those are the same letters as BRINAFUKK
00:46:07 -!- yorick has joined.
00:46:18 <elliott> Solace: you might like deadfish
00:46:23 <elliott> it is very easy
00:46:23 <Solace> Yeh i guess
00:46:32 <oerjan> Solace: i think myname is hinting that you seem to dislike the most common features of esolangs :P
00:46:33 <Solace> Ill go look at it
00:46:48 <Phantom_Hoover> <oerjan> brainfuck is hard because it's so low level that you have to implement almost everything from scratch, including any advanced data structures - you don't even have pointers or references.
00:47:12 <Solace> Nah not really its just like idk its name suits it well
00:47:12 <Phantom_Hoover> brainfuck, i'd say, is more than anything else hard because it has no built-in nonlocal stuff at all
00:47:25 <Solace> Verbosefuck is probably what ill be good at
00:47:32 <myname> Solace: you should try malbolge
00:47:42 <Solace> ...
00:47:49 <Solace> ©_©
00:48:05 <Jafet> Yeah, it's hard to imagine anyone using anything resembling brainfuck as any kind of formal basis for computation
00:48:45 <Solace> I need esolangs you can actually implement large data structures in
00:48:56 <Solace> Very large ones
00:48:57 <Phantom_Hoover> eodermdrome!!
00:49:25 <Solace> ?
00:49:38 * oerjan swats Jafet -----###
00:49:53 <Solace> :0 thats mean
00:50:00 <myname> Solace: how about funciton
00:50:06 <oerjan> Solace: you just think that because you didn't get his joke
00:50:16 <Solace> >_>
00:50:29 <Solace> I never get jokes
00:50:42 <Solace> Ill check that out also myname
00:50:44 <oerjan> (hint: turing machines resemble brainfuck in most of the ways that make it awkward)
00:51:31 <oerjan> not entirely, but enough
00:51:45 <Solace> I remember when i didnt know how to remove piping
00:52:18 <oerjan> Solace: eodermdrome is nice, you should implement it
00:52:22 <oerjan> (inside joke)
00:52:29 <Solace> :|
00:52:55 <Solace> i DONT know what eodermdrome is?!
00:53:03 <oerjan> ^wiki eodermdrome
00:53:08 <Solace> Lag
00:53:15 <oerjan> fizzie: !!!
00:53:22 <oerjan> no, missing fungot
00:53:36 <oerjan> @google eodermdrome
00:53:37 <lambdabot> http://esolangs.org/wiki/Eodermdrome
00:53:37 <lambdabot> Title: Eodermdrome - Esolang
00:53:54 <myname> Solace: it's pretty neat. all you have to do is solving an np hard problem every single step
00:54:31 <oerjan> Solace: you can implement large data structures in unlambda btw
00:54:57 <Solace> Really? oerjan
00:55:11 <Solace> Ok myname
00:55:46 <oerjan> i didn't say it would be easy hth
00:55:46 <Solace> Lets focus on one language at a time
00:55:59 <Solace> I have alot of time left
00:56:05 <oerjan> but it may still be easier than it most of the languages mentioned already
00:56:10 <oerjan> *in
00:56:17 <Solace> Oh ive seen unlambda
00:56:26 <Solace> Doesnt look terribly hard
00:56:49 <Solace> Is just kinda ehhh ok for me
00:56:57 <oerjan> i think unlambda was my first esolang, except for _probably_ having been exposed to parts of the INTERCAL manual at some point
00:57:24 <Solace> Anyways i have to dinner
00:57:38 -!- Solace has changed nick to Solace|Dinner.
00:57:54 <oerjan> um first to discover, that is
00:57:58 <myname> mine was brainfuck. at a point where i didn't really were able to write code in normal languages
00:58:37 <myname> there was a website explaining it like a turing mashine
00:58:52 <oerjan> charming
00:59:01 -!- fungot has joined.
00:59:03 <fizzie> I'm asleep, I can't help with missing fungots.
00:59:03 <fungot> fizzie: in the us
00:59:10 <oerjan> fizzie: OKAY
01:03:09 -!- boily has joined.
01:08:54 -!- mitchs has quit (Ping timeout: 256 seconds).
01:10:36 <oerjan> ahoily
01:11:22 -!- CrazyM4n has joined.
01:12:57 <boily> bonsœrjan!
01:16:16 -!- Frooxius has joined.
01:20:23 -!- mitchs has joined.
01:56:51 -!- Solace|Dinner has changed nick to Solace.
02:04:49 -!- Phantom_Hoover has quit (Read error: Connection reset by peer).
02:20:44 -!- roasted42 has joined.
02:28:57 -!- GeekDude has quit (Quit: {{{}}{{{}}{{}}}{{}}} (www.adiirc.com)).
03:00:19 -!- mitchs has quit (Ping timeout: 252 seconds).
03:01:43 -!- boily has quit (Quit: UNDEFINED CHICKEN).
03:03:53 -!- |oren\ has quit (Ping timeout: 240 seconds).
03:06:31 -!- vanila has quit (Remote host closed the connection).
03:09:52 -!- roasted42 has quit (Ping timeout: 245 seconds).
03:11:43 -!- roasted42 has joined.
03:12:12 -!- mitchs has joined.
03:25:11 <Sgeo> https://www.reddit.com/r/shittyprogramming/comments/2pxbr7/faster_inverse_square_root/
03:25:59 <nys> fisr
03:26:27 -!- adu has joined.
03:34:51 * pikhq wonders why his stomach hurts
03:35:56 <oerjan> too much tabasco
03:37:02 <oerjan> hidden eating utensils
03:37:23 <oerjan> ate too fast, swallowed fork
03:39:29 <pikhq> Y'mean I shouldn't have put tabasco on my fork and ate it?
03:39:32 <pikhq> Darn.
03:39:39 <pikhq> But I thought I was being a culinary genius.
03:39:52 <oerjan> sorry
03:46:23 <J_Arcane> this morning I learned Racket's case doesn't support one-half of the typical behavior of case statements.
03:46:52 <J_Arcane> https://github.com/jarcane/heresy/issues/10
03:50:36 -!- roasted42 has quit (Ping timeout: 250 seconds).
03:50:40 -!- mitchs has quit (Quit: mitchs).
03:51:30 <Jafet> That's because the case syntax is cond.
03:52:33 -!- roasted42 has joined.
03:54:07 -!- Sprocklem has joined.
03:59:10 <CrazyM4n> That reminds me that I was learning lisp like a week ago
04:01:35 <elliott> J_Arcane: pretty sure that holds in standard scheme too?
04:01:53 <elliott> J_Arcane: your syntax is weird, it's ((1) 'foo) because you can also do ((1 2 3) 'foo) I think
04:02:06 <elliott> so it would "at least" be (((mod 5 2)) 'foo)
04:03:34 <elliott> scheme's case is disappointing though
04:03:35 <J_Arcane> Yes, you can. and that's a good point.
04:03:40 <elliott> it is not exactly pattern matching
04:03:57 <J_Arcane> Probably because it does have match, and case is evil C.
04:03:57 <elliott> I suspect racket probably has something for proper pattern matching
04:04:08 <elliott> nah, case is scheme heritage for racket, not C
04:04:09 <J_Arcane> Yes, Racket has a very powerful match statement.
04:05:01 <elliott> yes, so I see
04:05:18 <elliott> |
04:05:18 <elliott>
04:05:18 <elliott> (pregexp px-expr)
04:05:18 <elliott>
04:05:18 <elliott> match string
04:05:22 <elliott> even supports pregnant expressions
04:07:16 <elliott> racket has a lot of nice stuff but I find it hard to see what its overarching philosophy is
04:07:43 <oerjan> wtf is a pregnant expression
04:07:51 <elliott> like a regular expression except pregnant
04:07:59 <oerjan> OH
04:08:25 <elliott> you can match them with the pcre library (pregnancy-compatible regular expressions)
04:09:04 <oerjan> good, good
04:12:36 -!- b_jonas has quit (Ping timeout: 258 seconds).
04:12:51 -!- b_jonas has joined.
04:13:06 <J_Arcane> Hah hah! I did it. I wrote an evaluating case statement. :D
04:13:26 -!- mitchs has joined.
04:13:29 <elliott> does it differ much from using cond?
04:13:33 <CrazyM4n> I tried googling that and through an untimely slew of typos, google thought I wanted "pregnant expressional lips"
04:14:24 <J_Arcane> elliott: less verbose in some cases. IT came up because I was writing a "canonical" FizzBuzz for Heresy, and realized I couldn't use the case method (ie. 0 as val, and various (mod ...) calculations for the matching clauses)
04:14:55 <J_Arcane> And it turns out it is literally as simple as rewriting it without the extra ' around the matching values.
04:18:11 -!- InvalidC1 has joined.
04:18:44 -!- roasted42 has quit (Ping timeout: 256 seconds).
04:19:00 -!- roasted42 has joined.
04:19:53 -!- InvalidCo has quit (Ping timeout: 258 seconds).
04:21:38 <J_Arcane> (in Racket, the helper macro that handles the equal? literally just matches on (k ...) but then does (equal? v 'k) instead.
04:27:17 -!- roasted42 has quit (Ping timeout: 240 seconds).
04:32:22 -!- tromp_ has quit (Read error: Connection reset by peer).
04:47:18 -!- mitchs has quit (Ping timeout: 264 seconds).
04:57:27 -!- sebbu has quit (Ping timeout: 258 seconds).
05:06:05 -!- relrod has quit (Excess Flood).
05:06:25 -!- relrod_ has joined.
05:08:41 -!- relrod_ has changed nick to relrod.
05:11:03 -!- j-bot has quit (Ping timeout: 245 seconds).
05:11:03 -!- rodgort has quit (Ping timeout: 245 seconds).
05:12:06 -!- rodgort has joined.
05:13:06 <Sgeo> `slist
05:13:08 <HackEgo> slist: Taneb atriq Ngevd Fiora Sgeo ThatOtherPerson alot
05:14:05 <Sgeo> Remind me to get back into Racket so I can get back to that optics library
05:24:24 -!- nys has quit (Quit: quit).
05:33:46 -!- mitchs has joined.
05:46:13 -!- copumpkin has joined.
06:01:51 -!- newsham has quit (Ping timeout: 258 seconds).
06:02:43 -!- newsham has joined.
06:05:44 -!- MoALTz has quit (Read error: Connection reset by peer).
06:06:26 -!- MoALTz has joined.
06:10:40 -!- MDude has changed nick to MDream.
06:22:30 -!- CrazyM4n has quit (Quit: Leaving).
06:29:59 <Solace> (∩ ͡° ͜ʖ ͡°)⊃━☆゚. * ・ 。゚, *
06:31:41 <Solace> How do you stop xml stack overflows
06:31:48 <Solace> This is so bad
06:33:53 <lifthrasiir> do not use xml
06:34:08 <Solace> Thanks that fixed the problem
06:35:06 -!- callforjudgement has joined.
06:35:19 -!- callforjudgement has quit (Changing host).
06:35:19 -!- callforjudgement has joined.
06:38:07 -!- ais523 has quit (Ping timeout: 272 seconds).
06:53:56 -!- sebbu has joined.
06:54:33 -!- sebbu has quit (Changing host).
06:54:33 -!- sebbu has joined.
07:04:52 -!- callforjudgement has quit (Read error: Connection reset by peer).
07:04:57 -!- scarf has joined.
07:05:13 -!- scarf has quit (Changing host).
07:05:13 -!- scarf has joined.
07:07:15 -!- mitchs has quit (Quit: mitchs).
07:07:47 -!- scarf has quit (Read error: Connection reset by peer).
07:08:01 -!- scarf has joined.
07:11:42 -!- adu has quit (Quit: adu).
07:11:55 -!- drdanmaku has quit (Quit: Connection closed for inactivity).
07:32:16 -!- Patashu has joined.
08:16:36 -!- oerjan has quit (Quit: leaving).
08:31:13 -!- azazel- has joined.
08:31:33 -!- azazel- has left ("...(Gone). Goodbye.").
08:46:41 -!- ais523 has joined.
08:48:52 -!- scarf has quit (Ping timeout: 240 seconds).
08:50:19 -!- oren has joined.
09:14:49 -!- Sprocklem has quit (Ping timeout: 245 seconds).
09:23:48 -!- arjanb has joined.
09:29:45 -!- nyuszika7h_ has changed nick to nyuszika7h.
09:36:35 <Jafet> Eodermdrome looks like it can be interpreted in polynomial time
09:37:01 <Jafet> (Each subgraph can have at most 26 nodes)
10:06:15 <myname> well, as long as you only allow lower case letter nodes
10:07:36 <Jafet> But programming would become too easy otherwise.
10:14:35 -!- InvalidC1 has changed nick to InvalidCo.
10:18:02 -!- oren has quit (Quit: Lost terminal).
10:48:34 -!- mitchs has joined.
11:00:08 -!- Solace has quit (Quit: Connection closed for inactivity).
11:00:17 -!- coppro has quit (Ping timeout: 240 seconds).
11:01:16 -!- coppro has joined.
11:18:39 -!- boily has joined.
11:18:45 <J_Arcane> https://twitter.com/abt_programming/status/546969469571325952
11:18:51 <ais523> Jafet: right, I intended to restrict it to 26 to keep things hard
11:18:55 <ais523> not sure if the spec actually achieves that, though
11:23:17 -!- weissschloss has quit (Ping timeout: 240 seconds).
11:23:17 -!- trn has quit (Ping timeout: 240 seconds).
11:25:34 -!- weissschloss has joined.
11:26:29 -!- trn has joined.
11:28:38 <b_jonas> ais523: but doesn't that mean you can have only finitely many programs (say at most double exponential in 26) so you can't encode arbitrary data in the program itself, so it's technically not turing-complete?
11:28:52 <b_jonas> it's TC only if you're allowed to prefix a string to the input
11:28:59 <ais523> it's curly-L-complete
11:29:07 <b_jonas> um
11:29:07 <ais523> also I think you might be able to get up to triple exponential
11:29:14 <b_jonas> what's "curly-L-complete"?
11:30:07 <ais523> http://esolangs.org/wiki/%E2%84%92
11:30:11 <b_jonas> triple exponential how? there's about 2**O(n**2) possible graphs and statements using n fixed letters,
11:30:24 <b_jonas> and a program is just a set of such statements
11:30:43 -!- mitchs has quit (Ping timeout: 272 seconds).
11:30:54 <b_jonas> hmm wait
11:31:05 <ais523> oh right, it's 2**(2**(n**2))
11:31:19 <b_jonas> you can have infinitely many programs because a statements can contain an arbitrary output string
11:31:20 <ais523> which is higher than double exponential I think?, but lower than triple exponential
11:31:31 <ais523> and arbitrary output strings won't affect the computational class
11:31:45 <b_jonas> exactly, it doesn't help making the language more turing-complete
11:32:08 <b_jonas> if you allow any number of letters, it is turing complete though
11:32:25 <b_jonas> and "efficient" too, in that it can simulate programs in polynomial time
11:32:34 <b_jonas> very slow polynomial, but still polynomial
11:38:14 <Jafet> In this case the construction of generalised Eodermdrome ("Geraliseodermdromen"?) is straightforward
11:42:20 -!- mitchs has joined.
11:51:38 -!- callforjudgement has joined.
11:53:46 -!- ais523 has quit (Ping timeout: 250 seconds).
12:14:13 -!- Phantom_Hoover has joined.
12:22:19 <J_Arcane> So in answer to my earlier puzzlement about Racket's (case ...) statement, apparently it has to do with performance details in how it compiles making it a lot faster if it's not allowed to do any calculation for the matching clauses at compile time.
12:23:37 -!- Patashu has quit (Ping timeout: 240 seconds).
12:24:13 -!- boily has quit (Quit: SUPERSYMMETRIC CHICKEN).
12:55:34 <mroman> !blsq 1Jq.+10C!CLq.+pa
12:55:34 <blsqbot> | {{144} ERROR: Burlesque: (.+) Invalid arguments! {144 89} ERROR: Burlesque: (.+) Invalid arguments! {144 89 55} ERROR: Burlesque: (.+) Invalid arguments! {144 89 55 34} ERROR: Burlesque: (.+) Invalid arguments! {144 89 55 34 21} ERROR: Burlesque: (.+) Inva
12:55:43 <mroman> !blsq 1Jq.+10C!CLq++pa
12:55:43 <blsqbot> | {144 233 288 322 343 356 364 369 372 374 375 376}
12:55:53 <mroman> !blsq 1Jq.+10!CCLq++pa
12:55:53 <blsqbot> | {1 2 4 7 12 20 33 54 88 143 232 376}
12:57:06 <mroman> !blsq 1Jq.+10!CCLqpdpa
12:57:06 <blsqbot> | {1 1 2 6 30 240 3120 65520 2227680 122522400 10904493600 1570247078400}
13:01:55 -!- mitchs has quit (Ping timeout: 272 seconds).
13:12:57 -!- singingboyo has quit (Ping timeout: 240 seconds).
13:13:57 -!- singingboyo has joined.
13:24:04 -!- callforjudgement has quit.
13:46:10 <mroman> *Main> eval $ parseRC "({x.x}{y.y}z)"
13:46:10 <mroman> (z)
13:46:51 <mroman> neat
13:49:11 <mroman> *Main> eval $ parseRC "({f.{x.{y.((fy)x)}}}{x.{y.x}}ab)"
13:49:12 <mroman> ((({x.{y.(a)}})(b))(a))
13:49:13 <mroman> crap
13:49:16 <mroman> this doesn't look right
13:54:34 <mroman> hm
13:54:53 <mroman> > (\f x y -> (f y) x)(\x y -> x)0 1
13:54:54 <lambdabot> 1
13:54:56 <mroman> see
13:54:59 <mroman> this should produce b
13:55:09 <mroman> but something is screewing up big time
13:56:33 <mroman> hm right
13:56:36 <mroman> bound vs unbound variables
13:58:27 <Jafet> @let eval=let e s@(_:'\\':v:'.':l)=let(x,')':t)=e$d l in(take 4 s++x++")",t);e('(':s)=let(x,t)=e s;(y,')':u)=e$d t in(a x y,u);e s=splitAt 1$d s;d=snd.span(==' ');a(_:'\\':v:_:l)s=let f x|x==v=s|1>0=[x]in fst.e$init l>>=f;a f x='(':f++" "++x++")" in fst.e
13:58:28 <lambdabot> Defined.
13:58:39 <Jafet> > eval "(((\\x. x)(\\y. y)) z)"
13:58:40 <lambdabot> "z"
13:59:34 <mroman> *Main> eval $ parseRC "({f.{x.{y.((fy)x)}}}{x.{y.x}}ab)"
13:59:35 <mroman> b
13:59:53 <mroman> much better.
14:01:30 <Jafet> > eval "((((\\f. (\\x. (\\y. ((f y) x)))) (\\c. (\\d. c))) a) b)"
14:01:32 <lambdabot> "b"
14:02:36 <mroman> > eval "((((\\f. (\\x. (\\y. ((f y) x)))) (\\x. (\\y. x))) a) b)"
14:02:37 <lambdabot> "a"
14:02:41 <mroman> :)
14:03:13 <mroman> this doesn't check either that it must not replace the x in the second term
14:06:33 <Jafet> I wonder how many strokes is needed to implement that
14:07:52 -!- arjanb has quit (Quit: bbl).
14:32:05 -!- tromp_ has joined.
14:38:05 <mroman> well
14:38:12 <mroman> at least now I have my own lambda calculus interpreter
14:53:16 -!- vanila has joined.
15:13:28 -!- MDream has changed nick to MDude.
15:17:55 -!- `^_^v has joined.
15:19:11 <J_Arcane> http://www.wired.com/2014/12/mathematicians-make-major-discovery-prime-numbers/
15:20:34 <vanila> Prime Numbers, which have previously only been hypothesized to exist were finally discovered in the wild.
15:22:06 <vanila> J_Arcane, there is way too much text in this, what result are they talking about?
15:22:20 -!- nycs has joined.
15:22:31 -!- `^_^v has quit (Disconnected by services).
15:22:36 -!- nycs has changed nick to `^_^v.
15:24:32 <J_Arcane> vanila: as best I could understand, it seems they've found a new proof for the gap between prime numbers.
15:25:01 <vanila> :S
15:25:13 <vanila> maybe his blog will explain it better
15:25:28 <vanila> Kevin Ford, Ben Green, Sergei Konyagin, James Maynard, and I have just uploaded to the arXiv our paper “Long gaps between primes“.
15:25:31 <vanila> http://terrytao.wordpress.com/2014/12/16/long-gaps-between-primes/
15:27:04 <vanila> so they are using graph theory ideas in sieving theory to get really good results on prime gaps
15:33:33 -!- drdanmaku has joined.
16:04:38 -!- GeekDude has joined.
16:25:26 -!- KingOfKarlsruhe has changed nick to KingBot.
16:25:46 -!- KingBot has changed nick to KingOfKarlsruhe.
16:31:41 -!- arjanb has joined.
16:34:40 -!- S1 has joined.
16:38:00 -!- mihow has joined.
16:44:27 -!- shikhin has joined.
16:45:14 -!- shikhin has changed nick to Guest5017.
16:47:22 -!- Guest5017 has changed nick to shikhout.
16:47:25 -!- shikhout has quit (Changing host).
16:47:25 -!- shikhout has joined.
17:00:23 -!- hjulle has quit (Remote host closed the connection).
17:03:40 -!- nys has joined.
17:04:44 -!- jix_ has quit (Quit: Lost terminal).
17:05:21 -!- jix has joined.
17:05:43 -!- Lorenzo64 has joined.
17:17:07 -!- oren has joined.
17:17:42 <oren> i am now north of north bay.
17:32:20 -!- shikhout_ has joined.
17:35:17 -!- shikhout has quit (Ping timeout: 240 seconds).
17:37:01 <int-e> oh wow, what's up with the C# entries for http://golf.shinh.org/p.rb?Base+37 ...
17:38:37 <int-e> (The whole output is just 659 bytes.)
17:45:01 -!- mihow has quit (Read error: Connection reset by peer).
17:46:01 -!- Phantom__Hoover has joined.
17:46:26 -!- mihow has joined.
17:47:56 -!- Phantom_Hoover has quit (Ping timeout: 256 seconds).
17:49:06 -!- mihow has quit (Client Quit).
17:58:48 <elliott> vanila: it was actually a whole bunch of results http://michaelnielsen.org/polymath1/index.php?title=Bounded_gaps_between_primes
17:59:32 <elliott> it's kind of amazing to see the comment threads, all these mathematicians just blasting through better and better bounds
18:00:11 <elliott> http://michaelnielsen.org/polymath1/index.php?title=Timeline_of_prime_gap_bounds
18:01:15 <vanila> oooh
18:03:51 <elliott> it's like in the movies where they get all the scientists to work together non-stop on finding a solution except it's pure mathematics :p
18:04:45 -!- mihow has joined.
18:05:26 <tromp_> it's number theory golfing
18:33:56 <vanila> this kind of math is intimidatingly difficult
18:38:17 <int-e> The "admissible sets" part (from k_0 to H) is actually fairly easy to understand. http://michaelnielsen.org/polymath1/index.php?title=Finding_narrow_admissible_tuples
18:39:05 <int-e> But the analytic number theory (which produces bounds on k_0) is very scary.
18:39:13 <vanila> I feel sad that im not studying math
18:45:25 -!- Solace has joined.
18:50:22 <oren> vanila: what are you majoring in?
18:50:34 <vanila> im not
18:50:59 <oren> oh, yeah that;s right, you're still young!
18:51:28 <vanila> i did math in the past
18:51:32 <oren> whereas i'm apparently old compared to everyone except oerjan
18:53:31 <elliott> oren: is that deduction because before you're majoring, you're a minor
18:53:34 * elliott hides
18:54:15 <oren> i never thought of it that way but yeah lololol
18:54:31 <elliott> (not exactly accurate but)
18:56:21 -!- Deewiant has quit (Quit: Viivan loppu.).
18:56:43 <vanila> http://www.reddit.com/r/math/comments/2m5gk3/terence_tao_is_going_to_be_on_colbert_report/ apparently tao has discovered a new prime
18:58:01 <elliott> following on the footsteps of grothendieck
18:58:04 <elliott> *in
18:58:34 <elliott> it's really cute when mathematicians know nothing about the elements of the sets they like
18:59:26 <oren> i was like "are twin primes the ones two numbers apart?"
19:00:19 <elliott> they're the ones born at the same time
19:01:12 <elliott> https://en.wikipedia.org/wiki/Sexy_prime I forgot this name =_=
19:02:13 <oren> Dang, i took a course in number theory and they didn't mention that? what a waste.
19:02:49 <oren> "sexyprime triplets"
19:03:55 <oren> knowing that there are such thing would be worth taking a course all on its own
19:07:09 -!- idris-bot has quit (Quit: Terminated).
19:11:39 <oren> what does idris-bot do?
19:12:35 <elliott> evaluates idris
19:15:20 -!- Deewiant has joined.
19:17:59 -!- nycs has joined.
19:19:44 -!- `^_^v has quit (Ping timeout: 256 seconds).
19:20:56 -!- Deewiant has quit (Quit: Viivan loppu.).
19:21:16 -!- Deewiant has joined.
19:22:03 -!- Deewiant has quit (Client Quit).
19:22:45 -!- Deewiant has joined.
19:22:49 -!- CrazyM4n has joined.
19:34:39 -!- Lorenzo64 has quit (Read error: Connection reset by peer).
19:43:03 -!- Lorenzo64 has joined.
19:44:11 <Phantom__Hoover> elliott, has it come to a conclusion of how much idris is worth yet?
19:44:41 <elliott> that joke is too bad to bother replying to, sorry
19:45:22 <Phantom__Hoover> i realise the timing may also have been a little off
19:45:34 <fizzie> This is the general advice channel, right? What's a good standard included-in-Debian duplicate-file-detector thingie?
19:46:15 <fizzie> (I ran across 'fdupes', but possibly I'm missing something that didn't have the good sense to put "dup" in the package name.)
19:59:57 -!- nycs has quit (Quit: This computer has gone to sleep).
20:03:37 -!- kcm1700_ has quit (Ping timeout: 265 seconds).
20:04:26 -!- mihow has quit (Quit: mihow).
20:04:43 -!- S1 has quit (Quit: S1).
20:04:48 -!- nycs has joined.
20:06:25 -!- kcm1700 has joined.
20:06:52 -!- Patashu has joined.
20:07:08 <oren> what about diff -s *
20:09:00 <oren> no that doesn't work
20:23:31 <oren> well you can use cmp and a loop: for i in * ; do for j in * ; do if cmp -s -- "$i" "$j" ; then echo "$i $j" ; fi; done ; done
20:23:51 <oren> that will output each pair twice tho
20:23:52 <fizzie> I don't think that'd be particularly efficient for, say, a terabyte of files.
20:24:03 <CrazyM4n> That RNA language is soo tedious to make an interpreter for D:
20:24:13 <fizzie> I think I'll try to go with this fdupes thing.
20:25:04 <oren> actually my loop is buggy anyway
20:25:07 -!- Patashu has quit (Ping timeout: 258 seconds).
20:27:34 -!- mihow has joined.
20:31:09 -!- Lorenzo64 has quit (Quit: Leaving).
20:31:51 <CrazyM4n> ;~; I'm 1/4th the way done typing the amino acids as a hash in ruby
20:32:35 <CrazyM4n> And it's taken like 5 minutes now D:
20:33:20 <CrazyM4n> Because 5 minutes is a long time that I should definitely be worried about.
20:33:39 <elliott> fizzie: "fdupes" is fun to say.
20:33:50 <elliott> fdupes. fdupes. faaadupes!
20:33:54 <elliott> hadoops.
20:41:34 <oren> man the c standard library sucks
20:42:10 <oren> i forgot, again, that strrev is one of those functions i keep copying the code of from one project to another.
20:42:45 <CrazyM4n> If you want a good stdlib why not just use C++?
20:45:16 <oren> C++ strings don't have reverse either actually
20:46:49 <elliott> oren: you'd be better off avoiding nul-terminated strings entirely, really
20:47:08 <CrazyM4n> Just encode them as arrays of integers
20:47:15 <CrazyM4n> It's probably a better alternative
20:47:18 <elliott> um...
20:47:24 <elliott> how is that different from using pointer to char?
20:47:30 <elliott> or do you mean a fixed-size char array
20:47:59 <CrazyM4n> By the way oren: http://en.cppreference.com/w/cpp/algorithm/reverse
20:48:25 <CrazyM4n> elliott: It's really not, I'm just joking around
20:48:37 <nycs> strings should really just be opaque blobs
20:48:56 <oren> that oughta do it actually...
20:49:44 <oren> i'm just writing some single-use glue code to get these files to have better names
20:49:53 -!- idris-bot has joined.
20:50:15 <oren> why in C/C++ because i'm an idiot i guess
20:51:29 <oren> never mind this will never work
20:53:57 <nycs> any time you want to iterate or index into a string you should ask yourself "is this going to work with unicode?"
20:54:05 <nycs> 99% of the time the answer is going to be no
20:54:32 <myname> not in rust!
20:54:39 <CrazyM4n> Would it work with your opaque blob idea?
20:55:18 <nycs> you'd probably want to disallow those operations outright
20:55:57 <nycs> well, not iterating i guess
20:56:08 <nycs> i dont know
20:56:14 <nycs> i havent thought too much about this
21:02:33 <elliott> nycs: depends what you're iterating over
21:02:41 <elliott> codepoints, graphemes, characters are all reasonable possibilities
21:04:02 <zzo38> 99% of the time I want to iterate or index into a string I want it to treat the string as single-bytes encoding anyways, so it will work.
21:05:02 <zzo38> (And if it does contain Unicode characters, it often works fine to just treat the individual bytes as characters anyways)
21:09:32 <CrazyM4n> https://gist.github.com/CrazyM4n/9a85ded307dcde3ece5b it's... finally... done...
21:22:13 <oren> i have some copypasta somewhere that converts utf-8 to an array of coedepoints as ints.
21:23:27 <oren> i wrote it because some crap i wrote wasn't working with unicode
21:24:10 <oren> CrazyM4n: conglaturation!
21:24:18 <CrazyM4n> woo
21:25:45 <elliott> int isn't necessarily big enough to store unicode codepoints :P
21:29:52 <oren> elliott: yeah, yeah, yeah... anyway assuming an unsigned is big enough, this is the code: https://gist.github.com/orenwatson/b071c93b287604684e6a
21:30:05 <elliott> you know uint32_t exists, right? :p
21:30:08 -!- Solace has quit (Quit: Connection closed for inactivity).
21:30:11 <elliott> > (length "uint32_t", length "unsigned")
21:30:12 <lambdabot> (8,8)
21:30:30 <CrazyM4n> as someone who doesn't do C or low level stuff
21:30:34 <CrazyM4n> I just vomited a little
21:30:35 <oren> yeah, i wrote this about 4 years a go tho
21:30:58 <oren> and it has been copypasted into various things
21:30:59 <elliott> anyway, this is comparable to the original plan 9 utf-8 implementation
21:31:05 <elliott> with its Rune type
21:31:11 <elliott> (it lives today on in Go)
21:36:43 <oren> technically this code doesn't convert to an array of ints, it returns one int at a time
21:37:36 <oren> yay for inconsistent ad-hoc apis
21:39:45 -!- idris-bot has quit (Quit: Terminated).
21:50:43 -!- idris-bot has joined.
21:51:47 <oren> hmm, could the lempel-ziv-welch compressor be turned into a programming language if some codewords instead altered the dictionary?
21:52:38 <vanila> good question!!
21:52:59 <oren> i have a shitty implementation of it just lying around..
21:54:25 <oren> like, maybe if we had a way to swap two existing codewords' definitions?
21:54:47 <vanila> what about conditionals?
21:54:53 <vanila> and loops
21:56:01 <oren> hm... loops could be done by having a codeword to move N codewords back, but onditionals...
21:57:40 <oren> actually for maximum crappiness, let's have it be N bits instead of N codewords
22:05:43 -!- CrazyM4n has quit (Quit: so that's how you do quit messages).
22:09:46 -!- Phantom__Hoover has quit (Ping timeout: 258 seconds).
22:21:49 -!- Phantom_Hoover has joined.
22:25:21 -!- nycs has quit (Quit: This computer has gone to sleep).
22:25:53 <HackEgo> [wiki] [[Special:Log/newusers]] create * Nysnamovois * New user account
22:26:12 <vanila> Nysnamovois sounds like a spammer
22:33:44 <oren> as he hasn't psoted any spam yet
22:33:52 <elliott> sounds like nys
22:35:56 <HackEgo> [wiki] [[Spite]] N http://esolangs.org/w/index.php?oldid=41526 * Nysnamovois * (+426) create
22:36:13 <HackEgo> [wiki] [[User:Nysnamovois]] N http://esolangs.org/w/index.php?oldid=41527 * Nysnamovois * (+5) Created page with "hello"
22:36:14 <vanila> Iwas wrong!
22:36:22 <nys> hello
22:36:26 <vanila> hi!
22:36:30 <vanila> you created a cool esolang
22:36:34 <nys> is it cool
22:37:31 <nys> if anyone wants me to uh explain anything
22:38:04 <nys> oh right <<> is like cdaar
22:38:50 <nys> i'm kinda spooked by the prospect of writing a curried function in it
22:40:07 <nys> oh shoot i forgot to add the minus symbol to the parser hold on
22:41:02 -!- boily has joined.
22:41:38 <HackEgo> [wiki] [[Spite]] M http://esolangs.org/w/index.php?diff=41528&oldid=41526 * Nysnamovois * (+0)
22:41:42 <nys> ok there
22:43:49 <oren> ok so as i understand it $ is the start symbol?
22:44:54 <oren> ohh, it means "apply"?
22:45:46 <nys> yes :D
22:49:23 <nys> ^ is like "on" from Data.Function
22:49:34 <nys> (which i discovered by looking up its type)
22:49:40 <nys> er, `, not ^
22:49:48 <nys> ^ is composition
22:50:21 <nys> but i think of them as "computed application" and "literal application"
23:00:00 -!- oerjan has joined.
23:01:17 <oerjan> arjanb: this channel is not big enough for both of us
23:02:12 <oerjan> (my search for my nick/name in the logs hits you as well)
23:03:54 <zzo38> Then use a better search
23:05:20 <oerjan> IE supports no beter ones
23:05:24 <oerjan> afaik
23:05:26 <oerjan> *+t
23:06:58 <oren> use a better browser hth
23:07:11 <oerjan> i think i'll just ban you all instead hth
23:08:37 <oren> use maxthon that is what i use on windows
23:08:45 <oerjan> wat
23:09:23 <oren> maxthon cloud browser. b/c i'm soooo original and clever
23:10:33 <oren> it -is- pretty awesome to
23:10:35 <elliott> isn't maxthon that like
23:10:38 <elliott> chinese IE shell
23:10:42 <oren> yup
23:11:15 <elliott> nys: this language looks cute
23:11:20 <oren> but unlike IE they didn't ruin it on win8
23:12:57 * arjanb waves at almost namesake
23:12:58 <elliott> did ie even change in win8
23:13:02 <nys> thanks elliot :D
23:13:08 <elliott> oh I guess there's the metro one but there's still the desktop version... (but why would you use IE)
23:13:34 <oren> because windows comes with IE.
23:14:19 -!- dts|pokeball has quit (Ping timeout: 264 seconds).
23:15:21 <oerjan> i don't want to change browser. i want the universe to stop continuously inventing new ways to annoy me while keeping most of the old ones.
23:17:21 -!- boily has quit (Read error: Connection reset by peer).
23:17:47 <oerjan> AND NOW IT'S DEPRIVING ME OF MY CHICKENS, THIS WILL NOT DO
23:17:59 <oerjan> (well, boily's chickens)
23:19:22 <oerjan> arjanb: hm do you come from #haskell? i recognize a similar nick from when i've read links from there
23:19:52 <arjanb> yep
23:20:21 <oerjan> elliott: IT'S UNSTOPPABLE *MWAHAHAHA* HTH
23:20:45 <int-e> WINSLOW CHICKEN?!
23:21:00 <oerjan> wat
23:21:05 <int-e> Ah, evil peer.
23:21:06 <oerjan> gg ->
23:21:20 -!- dts|pokeball has joined.
23:21:22 <oerjan> ...not updated
23:21:38 <oerjan> int-e: HOW DARE YOU RAISE MY HOPES
23:21:39 <int-e> I'm not paying attention, and I'm reading scrollback backwards, which does wonders to my perception of the context.
23:21:49 <oerjan> okay
23:22:17 <oerjan> ah unstoppable chicken, very winslow
23:23:07 <oerjan> at least xkcd has updated
23:26:38 <int-e> Yes, it did. Hope the next one will be better.
23:27:12 <oerjan> it's better with less oxygen hth
23:29:00 * oerjan is slightly confused by people like ee who submit golf answers that are nowhere near competitive
23:29:13 <oerjan> i guess as long as they're having fun.
23:31:16 <int-e> oerjan: yes, strange.
23:31:56 <vanila> I wante to sove combinator puzzles like "find a fixed point"
23:31:56 -!- shikhout_ has quit (Read error: Connection reset by peer).
23:32:04 <vanila> or given Lxy = (xy)y
23:32:11 <vanila> find a term which applies to itself gives itself back
23:32:27 -!- shikhout has joined.
23:32:34 <vanila> what would be the best way to program a search like that?
23:32:38 <tromp_> I I = I
23:32:50 -!- shikhout has changed nick to Guest86681.
23:32:51 <vanila> tromp_, but try to do it onl out of L terms
23:33:20 <oerjan> vanila: hm i had a combinatory logic question once, that i've never got answered: do the fixpoints of a value determine it? if not always, is there a model in which they do?
23:33:49 <oerjan> preferably a model generated by S and K
23:33:50 <vanila> I was thinking of converting from combinators to de bruijin and using some kind of algorithm to quickly test if they are equal (I know this is undecidable in general but I need to approximate it)
23:34:29 <vanila> like to test if m n equals m n' i ony need to test if n = n'? not sure if thats even true :/
23:34:49 <vanila> i suppose i could test n = n' as well as doing beta reduction to test m n = m n' in parallel
23:35:01 <elliott> it is, per leibniz, but maybe you mean something subtler than the obvious reading?
23:35:26 <vanila> oerjan, I can't really understand your question I think - doesnt' that there's multiple fixed point combinators mean you can't use fixed points to tell things apart?
23:35:47 <elliott> oerjan means, do the values x such that f x = x determine f
23:36:02 <int-e> oerjan: what do you mean by "fixed points of a value"? What are the fixed points of K and K K?
23:36:15 <elliott> as in, does {x | f x = x} uniquely determine f
23:36:15 <oerjan> the fixed point of K K is K, of course
23:36:28 <int-e> Ah.
23:36:45 <vanila> aren't the fixed points of Y and Theta the same?
23:36:53 <vanila> where Y and Theta are two different fixed point combinators
23:37:22 <elliott> well, you'd consider indistinguishable fixed point combinators equal
23:37:23 <oerjan> for K you have V (unlambda notation), i think all others are equivalent böhm tree-wise?
23:37:23 <int-e> oerjan: but neither K nor S have any fixed points.
23:37:27 <elliott> by functional extensionality, presumably
23:37:32 <vanila> ok
23:37:35 <elliott> right, bohm tree
23:37:47 <oerjan> int-e: um every combinator f has a fixed point, namely Yf
23:38:04 <int-e> meh.
23:38:16 <oerjan> of course you want beta-equivalence, probably eta.
23:38:22 <vanila> tthis is a really interesting question but does anyone know how to do what i wanted to do :[
23:38:28 <elliott> YS sounds scary
23:38:43 <vanila> i mean what algormth should i use to quickly test if combinator/lambda terms are probably equal
23:39:04 <HackEgo> [wiki] [[User:BCompton]] N http://esolangs.org/w/index.php?oldid=41529 * BCompton * (+1031) Created page with "==Languages I Created== *[[StaPLe]] ==Languages I've implemented== *[[Brainfuck]] - Python *[[Befunge]] - Python *[[Whitespace]] - Python *[[Tag]] - Python *My Unreliable P..."
23:39:05 <int-e> reduce to normal form, hoping there is one.
23:39:24 <elliott> oerjan: hm, YKx is y = Kyx = _|_, so YK = _|_ and I guess YK is the only fixed point of K?
23:39:25 <HackEgo> [wiki] [[User:BCompton]] http://esolangs.org/w/index.php?diff=41530&oldid=41529 * BCompton * (+3) D'oh!
23:39:28 <elliott> ergo K = _|_?
23:39:48 <elliott> vanila: sorry, I have no idea :(
23:39:50 <oerjan> vanila: LLL might count as a solution dependent on your semantics, since it never halts
23:39:52 <vanila> so just reduce a limit of a million times?
23:40:16 <oerjan> elliott: YK is not _|_
23:40:21 <vanila> The Lenstra–Lenstra–Lovász (LLL) lattice basis reduction algorithm ?
23:41:10 <elliott> oerjan: what is it? :(
23:41:13 <oerjan> vanila: LLL where L is the function you defined above
23:41:19 <int-e> vanila: Apparently there is a so called Gross-Knuth strategy for beta-reduction that is cofinal.
23:41:20 <vanila> oh
23:41:28 <vanila> the answer was ((L(LL))(L(LL)))((L(LL))(L(LL)))
23:41:31 <elliott> haha I thought LLL was some fancy equivalence-checking algorithm too
23:41:40 <oerjan> elliott: YKx = K(YK)x = YK
23:41:55 <oerjan> as i said, V from unlambda
23:42:00 <elliott> oerjan: how can you distinguish that from _|_, purely
23:42:22 <int-e> you can't
23:43:07 <elliott> is there a reason to consider it any different to any other variation of "function that returns itself when given any argument" (_|_, YK, etc.)
23:43:24 -!- bb010g has joined.
23:43:26 <elliott> it seems like you're staying YK isn't _|_ because it returns YK, not _|_ :p
23:43:39 <int-e> elliott: Depends on your model. In a term model, clearly those are not equivalent.
23:43:53 <elliott> are they equivalent with the usual denotational semantics?
23:44:27 <vanila> A strategy F is cofinal if whenever M->>N there is an n with N->>F^n(M).
23:44:52 <vanila> I don't really understand this
23:45:04 <vanila> i mean how does this apply to the equality test problem?
23:47:16 <int-e> Hmm. True that's not enough to make F^n(N) and F^m(M) have commone elements if N and M are equivalent.
23:48:35 <vanila> i know the problem is undecidable but i just want to be able to quickly verify claims like (KBB(SSS))SBS satisfies xL = xx or whatevr
23:48:45 <vanila> or return 'i dont know'
23:48:59 <oerjan> elliott: i suppose it's consistent for YK and _|_ to be equal.
23:49:26 <vanila> and i would implement it in C maybe, so it's efficient
23:49:39 <vanila> or ocaml
23:49:40 <elliott> oerjan: to be fair it's consistent for everything to be _|_
23:49:50 -!- adu has joined.
23:50:00 <oerjan> elliott: well modulo S /= K
23:50:15 <elliott> oerjan: no, S = K = _|_
23:50:16 <oerjan> which is a minimal distinction
23:50:42 <oerjan> elliott: i mean, if S = K then everything is _|_, so if you want something nontrivial just assume S /= K
23:50:48 <elliott> right.
23:50:54 <elliott> fair enough
23:51:33 <oerjan> of course there are other similar pairs.
23:51:42 <oerjan> but YK vs. _|_ may not be one.
23:52:32 <elliott> I mean I feel like to distinguish two terms you need to show some application of them that differs in some way other than one having x and one having y
23:52:33 <oerjan> i guess i mean consistent in a way similar to logic's "not everything is equivalent"
23:52:36 -!- mihow has quit (Quit: mihow).
23:52:53 <elliott> though even that rule isn't enough for me, since you can make a series F_0, F_1, ... s.t. F_n x = F_(n+1) I think
23:52:57 <elliott> (it just grows forever)
23:53:06 <vanila> elliott, so to show that f =/= g, you need to show that f x =/= g x ?
23:53:22 <elliott> vanila: for some x, yes, that would be my criteria
23:53:38 <elliott> and appealing to f =/= g for the f x =/= g x case doesn't seem very convincing to me, personally
23:53:41 <vanila> but to show that f x =/= g x dont I have to show that f x y =/= g x y?
23:53:56 <elliott> vanila: you know that S =/= K
23:53:58 <elliott> so you can go from there
23:54:02 <vanila> ah okay
23:54:07 <elliott> (like oerjan said)
23:57:57 <int-e> elliott: you can do so quite brutally: let f n x = f (n+1) in f 0, so Y (\f n x -> f (n+1)) 0, with church numerals, and abstraction elimination
23:58:40 <elliott> SII =/= I because SIIK = IK(IK) = K(IK) and IK = K, and K(IK)I = IK = K but KI = KI, and KI = KI but KII I'm not geting anywhere near
23:58:43 <elliott> *anywhere here
23:58:49 <elliott> where's my degree
23:58:53 <elliott> let's just assume it's true
23:59:00 <oerjan> Y K = K (Y K) = \x -> Y K which is a weak head normal form but not a head normal form i think...
23:59:20 <vanila> there's this thing used in lisp programming sometimes called SXHASH
23:59:22 <oerjan> and it has no head normal form, so if you go by requiring that...
23:59:39 <vanila> I wonder if there's something similar, a nontrivial hash of de brjuin terms which doesn't change when you perform a beta reduction
←2014-12-21 2014-12-22 2014-12-23→ ↑2014 ↑all