←2007-03-20 2007-03-21 2007-03-22→ ↑2007 ↑all
00:00:49 * SevenInchBread is playing around with fuzzy string matching.
00:00:58 <SevenInchBread> to find typos.
00:02:54 -!- ShadowHntr has joined.
00:04:01 -!- sebbu2 has quit ("@+").
00:07:12 -!- nazgjunk has quit (Connection timed out).
00:10:21 -!- FabioNET has quit (Client Quit).
00:47:32 -!- ShadowHntr has quit ("End of line.").
01:28:44 -!- mule| has joined.
02:23:57 <bsmntbombdood> odd
02:24:34 <oerjan> even
02:24:47 <mule|> prime
02:25:04 <oerjan> carmichael
02:25:29 <bsmntbombdood> cons M N = \a.aMN
02:25:40 <bsmntbombdood> car = \a.a(\bc.cIb)
02:25:49 <bsmntbombdood> wtf?
02:27:19 <bsmntbombdood> car (cons M N) == NIM?
02:27:34 <oerjan> eh..
02:27:50 <oerjan> i think that should be car = \a.a(\bc.b)
02:28:03 <bsmntbombdood> it would seem...
02:28:12 <bsmntbombdood> this is from _the calculi of lambda conversion_, church
02:29:19 <bsmntbombdood> oh
02:29:25 <bsmntbombdood> M and N are church numerals
02:29:30 <bsmntbombdood> so it works
02:29:59 <bsmntbombdood> oh, right, this isn't lambda_K calculus
02:30:14 <oerjan> it's in his lambda_I calculus perhaps?
02:30:29 <oerjan> you beat me to it :)
02:30:59 <oerjan> except...
02:31:07 <oerjan> does it work if N is a cons?
02:31:56 <bsmntbombdood> no
02:32:15 <bsmntbombdood> car (cons (cons A B) M) == ABM
02:33:10 <oerjan> i think that is the wrong order
02:33:52 <oerjan> it works if M is a cons but probably cdr would break then
02:36:13 <oerjan> anyhow pairing of church numerals can be done differently in a numerical way
02:36:32 <oerjan> say (M,N) = 2^M(2*N+1)
02:36:40 <bsmntbombdood> exponentionally?
02:36:42 <oerjan> might be harder to undo i guess
02:37:04 <oerjan> it was just the simplest
02:37:13 <bsmntbombdood> 2^M + 3^N
02:37:22 <oerjan> you mean *
02:37:28 <bsmntbombdood> yeah
02:37:47 <oerjan> or else you might have some hard mathematical problem
02:39:05 <oerjan> or maybe not so hard
02:39:29 <bsmntbombdood> hrm
02:39:57 <bsmntbombdood> I was always taught that you could only solve for one unkown per equation
02:40:22 <bsmntbombdood> but 2^M * 3^M can be solved for 2
02:40:22 <oerjan> doesn't hold with integer equations
02:42:05 <oerjan> with reals and continuous functions you can show you cannot get more than one variable for sure, unless the function is at an extreme value
02:43:22 <oerjan> because with two variables you can go between two points in two distinct paths
02:44:11 <oerjan> and both paths must contain all intermediate values for the function - so the solution for an intermediate value cannot be unique
02:44:51 <oerjan> but with only integers, you can jump over values
02:44:57 <bsmntbombdood> yeah
02:45:06 <bsmntbombdood> interesting predecessor function...
02:46:19 <bsmntbombdood> \a.3_3(a (\b.[Succ(3_1 b), 3_1 b, 3_2 b]) [1,1,1])
02:46:46 <bsmntbombdood> 3_n takes the nth element of a triple
02:47:01 <oerjan> thought so
02:47:13 <oerjan> but you beat me to it again :)
02:50:19 <oerjan> he doesn't use 0 i see
02:50:40 <oerjan> i suppose 0 cannot be constructed since it doesn't use its first argument
02:50:52 <bsmntbombdood> right
02:51:24 <SevenInchBread> YOU PEOPLE AND YOUR LAMBDA CALCULI
02:51:29 <SevenInchBread> DISGUST ME
02:51:30 <bsmntbombdood> he says positive, not not-negative
02:51:57 <oerjan> IS THAT A REQUEST?
02:52:03 <GregorR> It appears to be.
02:52:14 <GregorR> He's telling people who have lambda calculi to disgust him.
02:53:55 <SevenInchBread> yep
02:55:45 <bsmntbombdood> ohh neat
02:56:05 <bsmntbombdood> par = \a.a (\b.3-b) 2
02:56:16 <bsmntbombdood> par <even> == 2
02:56:21 <bsmntbombdood> par <odd> == 1
02:56:47 <bsmntbombdood> and a-b is a (Pred) b
02:57:00 <bsmntbombdood> b (Pred) a, I mean
02:57:22 <oerjan> hmph. 2+3 = 1+4 and 2+9 = 8+3
02:58:58 <bsmntbombdood> ...?
02:59:14 <oerjan> and 2+15 = 16+1, 32+3 = 8+27
02:59:24 <oerjan> so 2^m + 3^n cannot work
03:00:55 <bsmntbombdood> those are all primes
03:01:09 <mule|> 35 isn't prime?
03:01:15 <bsmntbombdood> except 35
03:01:19 <SevenInchBread> 7 * 5
03:01:30 <SevenInchBread> ...or is this a different base?
03:01:43 <oerjan> well they cannot be divisible by 2 or 3
03:01:51 <oerjan> no, ordinary decimal
03:01:53 <bsmntbombdood> oh, i misread
03:02:00 <bsmntbombdood> * for + again
03:02:45 <oerjan> and 259 has two forms too, although i haven't found both
03:03:02 <oerjan> just made Haskell list and sort
03:03:58 <oerjan> I'll try a proper program instead of a one-liner
03:04:09 <bsmntbombdood> this lambda_I calculus is too complicated
03:05:35 <oerjan> yeah, it's even more esoteric than the usual one
03:14:39 <bsmntbombdood> whoa
03:15:48 <bsmntbombdood> it's possible to convert a combination into a number, and have a one-to-one mapping between them
03:16:01 <oerjan> certainly
03:16:27 <oerjan> it's just a bit more complicated
03:16:49 <oerjan> well, actually, my 2^m(2n+1) does that i think
03:17:21 <bsmntbombdood> g\"odel numbers
03:17:24 <oerjan> make that 2^(m-1)(2n+1)
03:17:37 <oerjan> eh,
03:17:43 <oerjan> 2^(m-1)(2n-1)
03:18:32 <oerjan> but it can also be done with polynomials
03:18:56 <bsmntbombdood> (m+n)(m+n-1)-2n+2
03:19:07 <oerjan> i suppose
03:20:16 <bsmntbombdood> that's what's given here (for application)
03:21:11 <oerjan> essentially you put the (m,n)'s in a square infinite in two directions
03:21:25 <oerjan> and then you count them along the diagonals
03:21:33 <oerjan> then you get something like that.
03:22:47 <oerjan> it's a standard way of showing that aleph_0 * aleph_0 = aleph_0 where aleph_0 is the cardinality of the natural numbers
03:23:52 <oerjan> more generally, the theorem that m*m = m for an infinite cardinality is equivalent to the axiom of choice
03:24:57 <oerjan> i think it was
03:29:07 <bsmntbombdood> I wonder why church even bothered with lambda_I calculus
03:29:41 <bsmntbombdood> the definition of lambda_K calculus is simpler
03:31:46 <bsmntbombdood> oh
03:32:15 <bsmntbombdood> "it becomes clearly unreasonable the FN should have a normal form and N have no normal form"
03:35:04 <oerjan> he was trying to avoid lazy evaluation :D
03:35:37 <bsmntbombdood> dirty, dirty haskell
03:41:57 <bsmntbombdood> some theorems of the lambda_I calculus fail
03:47:29 <bsmntbombdood> oh boy, transfinite ordinals in the lambda_K calculus
03:47:53 <SevenInchBread> ...I like, "procrastinated evaluation".
03:49:14 -!- ShadowHntr has joined.
03:49:59 <oerjan> but the lambda_I calculus is also dirty. Some theorems of linear logic fail.
03:50:10 <mule|> "procrastinated evaluation" : return result later;
03:50:11 <mule|> ?
03:50:12 <mule|> lol
03:50:31 <SevenInchBread> ...something like that.
03:51:04 <oerjan> That was some of the point of my vaporware language Reaper.
03:51:40 <SevenInchBread> I'd like to combine the advantages of lazy evaluation with eager evaluation.
03:51:56 <oerjan> You know about lenient evaluation?
03:52:03 <SevenInchBread> ...nope.
03:53:49 <oerjan> It evaluates most subexpressions in parallel.
03:54:04 <bsmntbombdood> oh man
03:54:10 <bsmntbombdood> there's a lambda-delta calculus too
03:54:20 <oerjan> This surprisingly gives it some of the advantages of lazy evaluation.
03:54:56 <SevenInchBread> hmmm... you could evaluate different parts of the expression that can be evaluated... and wait for the rest to become available (in the form of unspecified arguments and stuff)
03:55:09 <SevenInchBread> ...taking away the linearness of execution.
03:55:34 <oerjan> By being even _more_ eager, it doesn't give any particular subexpression the ability to cause an infinite loop for the whole program
03:56:11 * SevenInchBread has a fetish for coroutines.
03:57:22 <bsmntbombdood> TOO MUCH MAN TOO MUCH
03:57:58 <SevenInchBread> THERE CAN NEVER BE TOO MUCH OF MAN
03:58:14 <oerjan> AND STILL YOU HAVEN'T GOT TO SYSTEM F
03:58:29 <bsmntbombdood> delta M N is replaced be (\ab.ab) provided that M and N are in delta normal form and contain no free variables and M is not alpha convertable into N
03:58:36 <SevenInchBread> SYSTEM F?
03:59:01 <oerjan> typed polymorphic lambda calculus
03:59:08 <SevenInchBread> ...
03:59:13 <bsmntbombdood> delta M M is replaced by (\ab.a(ab)) provided that M is in delta normal form and contains to free variables
04:04:23 <bsmntbombdood> hmm
04:04:42 <bsmntbombdood> seems like the lambda-delta calculus fixes some of the limitations of the lambda_K calculus
04:05:47 <bsmntbombdood> while still allowing throwing away arguments
04:07:25 <SevenInchBread> IO has a neato macro-ish like execution.
04:07:36 <SevenInchBread> non-strict functions
04:08:55 <bsmntbombdood> fun
04:09:15 <bsmntbombdood> the existential quantifier in the lambda-delta calculus
04:15:03 -!- _spaz has joined.
04:15:22 -!- _spaz has left (?).
04:18:41 <bsmntbombdood> http://www-tech.mit.edu/V125/N65/coursevi.html
04:23:20 <bsmntbombdood> oh man, i hope this is a joke: http://public.research.att.com/~bs/whitespace98.pdf
04:28:15 -!- SevenInchBread has quit (Read error: 113 (No route to host)).
04:30:05 <oerjan> probably. it starts getting surreal from the "Previous work" section
04:30:43 <oerjan> And completely absurd in the next
04:32:41 <oerjan> And the "Overloading missing whitespace" section should leave not the slightest amount of doubt.
04:34:07 <bsmntbombdood> who knows, strousup is pretty crazy
04:35:27 <oerjan> you must be heavily prejudiced to think he really means identifiers should be restricted to single UNICODE characters.
04:40:48 <oerjan> in fact he stretches it so far i don't see why he should need the April Fool at the end.
04:41:44 <oerjan> in fact you should already have been tipped off at the first April in the text.
04:43:23 <oerjan> which i missed since i just browsed :)
04:43:55 <bsmntbombdood> me too
04:44:20 <oerjan> the strange thing is that in another language the basic suggestion could have merit.
07:03:08 -!- GreaseMonkey has joined.
07:09:02 -!- GreaseMonkey has quit (Remote closed the connection).
07:24:45 -!- Sgeo has quit ("Leaving").
07:24:47 <oklopol> i love it when someone writes a long article in a serious style as a joke :P
07:42:42 -!- GregorR has quit (zelazny.freenode.net irc.freenode.net).
07:42:43 -!- tokigun has quit (zelazny.freenode.net irc.freenode.net).
07:43:07 -!- GregorR has joined.
07:43:07 -!- tokigun has joined.
07:44:28 -!- oerjan has quit ("quite").
07:44:42 -!- tokigun has quit (Connection reset by peer).
07:44:47 -!- tokigun has joined.
07:59:59 -!- clog has quit (ended).
08:00:00 -!- clog has joined.
08:07:13 -!- ShadowHntr has quit (Read error: 110 (Connection timed out)).
08:19:52 -!- ShadowHntr has joined.
08:57:49 -!- ShadowHntr has quit ("End of line.").
09:03:58 -!- GreaseMonkey has joined.
09:15:33 <nooga> http://public.research.att.com/~bs/whitespace98.pdf
09:15:36 <nooga> whoops
10:08:01 <GreaseMonkey> ok, gonna have to sleep now, gnight
10:10:21 -!- GreaseMonkey has quit ("vvgnight, and FU AUTORTB").
11:34:44 <nooga> i code xhtml in vim ;p
11:36:24 -!- jix has joined.
11:39:37 -!- nazgjunk has joined.
11:49:50 -!- UpTheDownstair has joined.
11:49:50 -!- nazgjunk has quit (Read error: 104 (Connection reset by peer)).
12:14:13 -!- UpTheDownstair has changed nick to nazgjunk.
12:53:26 -!- helios24 has joined.
12:59:54 -!- nazgjunk has quit (Connection reset by peer).
13:00:24 -!- nazgjunk has joined.
13:28:31 -!- nazgjunk has quit (Read error: 104 (Connection reset by peer)).
13:28:34 -!- UpTheDownstair has joined.
13:29:08 -!- UpTheDownstair has changed nick to nazgjunk.
15:42:01 -!- jix__ has joined.
15:50:14 -!- jix has quit (Read error: 110 (Connection timed out)).
16:06:10 -!- ShadowHntr has joined.
17:07:37 -!- UpTheDownstair has joined.
17:07:53 -!- nazgjunk has quit (Read error: 104 (Connection reset by peer)).
17:37:17 <SimonRC> nooga: funny nevertheless
17:40:06 -!- FabioNET has joined.
18:18:10 <nooga> :D
18:18:22 <nooga> it is NOT funny
18:19:53 <SimonRC> I was referring to the AFJ you posted, not the vim comment
18:20:32 <nooga> oh
18:21:03 <nooga> bsmntbombdood posted it before me
18:25:57 <bsmntbombdood> what
18:26:39 <nooga> that article on whitespace
18:27:45 <bsmntbombdood> oh
18:28:16 <SimonRC> I learnt an interesting thing in my computability class:
18:28:44 <bsmntbombdood> haha school
18:28:52 <SimonRC> (no, uni)
18:28:59 <bsmntbombdood> yeah
18:29:19 <SimonRC> Any function can be computed as the minimisation of some primitive-recursive predicate.
18:29:30 <SimonRC> this could lead to some interesing esolangs.
18:29:35 <bsmntbombdood> minimisation?
18:29:41 <SimonRC> yeah
18:29:45 <bsmntbombdood> what's that
18:30:04 <SimonRC> you have some predicate on Nat, and the minimisation is the smallest input that makes it return true
18:30:17 <SimonRC> minimise :: (Nat -> Bool) -> Nat
18:30:51 <SimonRC> minimise p = head $ filter p $ [0..]
18:31:42 <SimonRC> And the predicate can be primitive recursive, a class that includes most useful terminating functions.
18:32:01 <SimonRC> ... including the bounded-time evaluator.
18:32:49 <bsmntbombdood> so computation is based on the Nat -> Bool predicates?
18:35:06 -!- ShadowHntr has quit ("End of line.").
18:40:56 <bsmntbombdood> gar
18:41:08 <bsmntbombdood> i want the P'' paper
18:43:03 <SimonRC> bsmntbombdood: yes
18:43:24 <SimonRC> In computability theory, most data is Nat.
18:43:45 <SimonRC> the only operations are succ, pred, and jnz
18:43:51 <SimonRC> hehehe
18:44:16 <bsmntbombdood> jnz?
18:44:19 <SimonRC> since we only care about computability, the programs we write probably have lots of ackerman runtimes.
18:44:27 <SimonRC> and in ASM
18:44:34 <SimonRC> Jump if Non-Zero
18:44:41 <SimonRC> *"as in ASM"
18:45:03 <bsmntbombdood> ackermann runtime, that's pretty bad
18:45:17 <bsmntbombdood> I can't even imagine an algorithm being that slow
18:45:41 <SimonRC> maybe I exaggerate
18:48:00 -!- FabioNET has quit (Read error: 145 (Connection timed out)).
18:51:31 -!- oerjan has joined.
18:57:34 -!- helios24 has quit (Read error: 60 (Operation timed out)).
19:06:56 -!- helios24 has joined.
19:35:11 -!- sebbu has joined.
19:58:02 -!- nazgjunk has joined.
20:02:17 -!- oerjan has quit ("leaving").
20:04:42 -!- UpTheDownstair has quit (Read error: 145 (Connection timed out)).
20:06:57 -!- sebbu2 has joined.
20:10:48 -!- UpTheDownstair has joined.
20:14:45 -!- sebbu has quit (Read error: 60 (Operation timed out)).
20:26:40 -!- nazgjunk has quit (Read error: 110 (Connection timed out)).
20:41:42 <nooga> SADOL raytracer looks cool :D
20:45:35 <nooga> http://pastebin.ca/405483 Kix ass
20:47:24 <oklopol> i understand that completely
20:55:47 -!- helios24 has quit ("Leaving").
20:58:09 -!- SevenInchBread has joined.
21:17:05 -!- UpTheDownstair has changed nick to nazgjunk.
21:51:56 -!- digital_me has joined.
22:07:05 -!- nazgjunk has quit (Read error: 104 (Connection reset by peer)).
22:07:15 -!- UpTheDownstair has joined.
22:12:13 <SevenInchBread> What's a good HTTP server app?
22:19:54 -!- nazgjunk has joined.
22:27:09 -!- death has joined.
22:27:50 <bsmntbombdood> SevenInchBread: apache?
22:29:28 -!- death has quit (Nick collision from services.).
22:32:15 -!- foolzh has joined.
22:32:29 -!- nazgjunk has quit (Nick collision from services.).
22:32:47 -!- foolzh has changed nick to nazgjunk.
22:36:06 -!- UpTheDownstair has quit (Connection timed out).
22:47:45 -!- jix__ has quit ("Bitte waehlen Sie eine Beerdigungnachricht").
22:49:31 <SevenInchBread> so...
22:49:47 <SevenInchBread> how would you like... go about making an operating system? I'm having trouble knowing where to begin.
22:51:21 -!- Sgeo has joined.
22:52:22 <lament> SevenInchBread: begin with writing some simple program that sits in the MBR, i suppose.
22:55:37 <SevenInchBread> ...how would you do that?
22:59:05 <bsmntbombdood> lunix
23:06:27 -!- oerjan has joined.
23:11:04 <GregorR> http://lng.sourceforge.net/ < Lunix :P
23:11:42 <bsmntbombdood> i was looking at that a while back
23:12:05 <SevenInchBread> I really want to start work on an esoos
23:13:31 <nazgjunk> hehe
23:13:50 * oerjan is surprised there does not seem to be a Lunatix OS
23:19:40 -!- sebbu has joined.
23:22:18 <SevenInchBread> ...I just... can't conceive of what a kernel program would look like...
23:24:28 <lament> SevenInchBread: a big loop
23:24:43 <lament> or rather, not even
23:25:05 <lament> SevenInchBread: the important kernel stuff sits on the timer interrupt
23:25:21 <lament> SevenInchBread: and all it really has to decide is what program to switch to
23:25:59 <lament> add syscalls if you wish to implement any
23:26:06 <lament> syscalls are basically separate from the other stuff
23:27:12 <lament> and you need some kind of memory manamegement system for your programs, that in the simplest case would just designate an area of memory for them to use when a program is ran.
23:27:21 <lament> that's basically it, the devil's in the details...
23:28:08 <SimonRC> hm
23:28:23 <SimonRC> indeed
23:28:51 <lament> in its basic form it's like, fifteen lines of high-level code.
23:29:18 <SimonRC> I like the Synthesis kernel
23:29:36 <SimonRC> It puts code together at runtime so it goes like a rocket
23:29:52 <SimonRC> read up on it; the paper is very readable
23:30:30 * bsmntbombdood finds
23:33:42 -!- nazgjunk has quit (Read error: 104 (Connection reset by peer)).
23:34:11 -!- nazgjunk has joined.
23:46:08 -!- sebbu2 has quit (Read error: 110 (Connection timed out)).
23:49:43 <SevenInchBread> ...I have found that many programs operate on the principle of a big loop
23:50:33 <lament> the kernel is basically a loop, but instead of an explicit loop it's a single piece of code repeatedly activated by the timer interrupt.
23:53:07 <SevenInchBread> ...timer inrerruopt?
23:56:45 <SevenInchBread> ...yeah, should read up on my hardware stuff.
←2007-03-20 2007-03-21 2007-03-22→ ↑2007 ↑all