00:01:29 <{^Raven^}> hullo peeps and peepettes
00:03:47 -!- jix has left (?).
01:17:43 -!- yrz\werk has quit (Read error: 110 (Connection timed out)).
01:22:14 -!- int-e has left (?).
02:49:32 -!- calamari has joined.
03:06:17 -!- calamari_ has quit (Read error: 110 (Connection timed out)).
03:26:49 -!- calamari has quit ("Leaving").
04:14:04 -!- heatsink has joined.
04:21:42 -!- calamari has joined.
04:29:41 -!- lament has quit (kornbluth.freenode.net irc.freenode.net).
04:45:01 -!- lament has joined.
05:23:05 -!- heatsink has quit (kornbluth.freenode.net irc.freenode.net).
05:23:05 -!- tokigun has quit (kornbluth.freenode.net irc.freenode.net).
05:23:05 -!- cmeme has quit (kornbluth.freenode.net irc.freenode.net).
05:23:06 -!- ZeroOne has quit (kornbluth.freenode.net irc.freenode.net).
05:23:06 -!- puzzlet has quit (kornbluth.freenode.net irc.freenode.net).
05:23:06 -!- cpressey has quit (kornbluth.freenode.net irc.freenode.net).
05:24:29 -!- heatsink has joined.
05:24:29 -!- tokigun has joined.
05:24:29 -!- cmeme has joined.
05:24:29 -!- cpressey has joined.
05:24:29 -!- ZeroOne has joined.
05:24:29 -!- puzzlet has joined.
05:28:08 -!- cpressey_ has joined.
05:28:28 -!- heatsink has quit (kornbluth.freenode.net irc.freenode.net).
05:28:28 -!- cmeme has quit (kornbluth.freenode.net irc.freenode.net).
05:28:28 -!- puzzlet has quit (kornbluth.freenode.net irc.freenode.net).
05:28:28 -!- cpressey has quit (kornbluth.freenode.net irc.freenode.net).
05:28:28 -!- tokigun has quit (kornbluth.freenode.net irc.freenode.net).
05:28:28 -!- ZeroOne has quit (kornbluth.freenode.net irc.freenode.net).
05:29:49 -!- cmeme has joined.
05:29:49 -!- heatsink has joined.
05:29:49 -!- tokigun has joined.
05:29:49 -!- cpressey has joined.
05:29:49 -!- ZeroOne has joined.
05:29:49 -!- puzzlet has joined.
05:35:04 -!- cpressey has quit (Read error: 104 (Connection reset by peer)).
06:26:40 -!- cmeme has quit (Remote closed the connection).
06:27:28 -!- cmeme has joined.
06:27:49 -!- cmeme has quit (Remote closed the connection).
06:28:33 -!- cmeme has joined.
07:01:39 -!- heatsink has quit ("Leaving").
07:09:09 -!- calamari has quit (Read error: 110 (Connection timed out)).
07:59:59 -!- clog has quit (ended).
08:00:00 -!- clog has joined.
11:11:43 -!- jix has joined.
13:36:08 -!- int-e has joined.
15:29:37 -!- cmeme has quit ("Client terminated by server").
15:30:19 -!- cmeme has joined.
16:06:22 <{^Raven^}> is it just me or have there been a *lot* of netsplits recently?
16:30:32 <Gs30ng> well i haven't seen anything like that
16:30:51 <Gs30ng> maybe you can check the chat log
17:03:56 -!- calamari has joined.
17:20:05 <calamari> hi
17:20:12 <Gs30ng> hi
18:00:18 <calamari> hmm.. so if I understand it correctly, the basis for lambda calculus is just f(x)=M(x), where x=N, so M(x)=M(x=N)=M(N)
18:42:46 -!- speedboy has joined.
19:01:55 <calamari> S = lxyz.xz(yz) =? (lxyz.xz)yz =? xz[xyz=yz] =? xz[yz] 
19:02:26 <calamari> l = lambda
19:03:44 <int-e> no.
19:04:27 <int-e> S = lxyz.xz(yz) is an abbreviation for (lx.(ly.(lz.((xz)(yz)))))
19:05:39 <calamari> ahh... thanks
19:06:31 <int-e> Sabc = (((Sa)b)c) = ((((lx.(ly.(lz.((xz)(yz)))))a)b)c) = (((ly.(lz.((az)(yz))))b)c) = ((lz.((az)(bz)))c) = ((ac)(bc))
19:06:45 <int-e> for arbitrary terms a, b, c.
19:06:48 <int-e> +r
19:14:15 <calamari> K = lxy.z = (lx.(ly.x)y), Kab = (lx.(ly.x)a)b = (ly.a)b = ly.b ?
19:14:54 <int-e> no, the ly disappears in the last step
19:15:01 <calamari> ahh right
19:15:06 <calamari> so = b
19:15:08 <int-e> and the b with it, leaving a
19:15:31 <calamari> hmm,.. don't think I follow that
19:15:33 <int-e> Ka is a constant function taking one argument and giving a.
19:16:10 <int-e> (ly.a)b means that you take the term a and replace every y in it by b. as it turns out, there is no y in the term so the b is just eaten.
19:18:49 <calamari> (ly.a)b = a[y=b] = a[b] = ??? = a
19:19:00 <int-e> a[y=b] is just a.
19:19:10 <calamari> not a[b] ?
19:19:14 <int-e> no.
19:19:46 <int-e> a[y=b] is just a notation that denotes the term a, with every occurence of y replaced by b.
19:19:50 <calamari> hmm.. I don't understand the definition then.. I have (lx.M)N = M[x:=N]
19:20:15 <calamari> := doesn't mean = I take it
19:20:48 <int-e> hmm. well, it's  (ly.a)b = a[y:=b] = a then.
19:21:32 <calamari> interesting.. I need to see if I can figure out how that works
19:33:02 <calamari> it seems like there is a situation like this with regular functions, but I can't remember how to write it
19:34:26 <calamari> thanks for your explanations and corrections
19:34:45 <int-e> f(x,y) = x.
19:36:17 <int-e> lambda calculus was originally a notation for functions without having to invent a name for each. instead of 'the function f, where f(x) = <complicated term>' you could write 'the function \lambda x.<complicated term>'.
19:37:27 <calamari> function notation has been ingrained in me all my life.. it's hard to let go. :)  trying tho!
19:38:07 <calamari> so f(x,y,z)=xz(yz) seems to make sense now :)
19:41:39 <calamari> xy(yz) = x*y*z^2 ?  I'm assuming it was just chosen to be written that way
19:41:49 <int-e> no
19:41:58 <calamari> oops
19:42:05 <int-e> sorry. let's build this from bottom up
19:42:12 <calamari> I messed that up anyways
19:42:18 <calamari> it would have been y^2 
19:42:44 <int-e> you have a set of symbols that serve as variables and you define terms in the following way:
19:43:03 <int-e> 1. every variable is a term. in our case, x, y, and z are terms.
19:43:27 <int-e> 2. if t is a term and x is a variable, lx.t is a term.
19:43:42 <int-e> 3. it t and r are terms then (tr) is a term.
19:43:55 <int-e> 2. is called lambda abstraction. 3 is called (function) application.
19:44:30 <int-e> for convenience we write xyz instead of ((xy)z), that is, function application is left associative.
19:44:54 <calamari> what is (tr), is that (t*r) ?
19:45:11 <calamari> or t(r) ?
19:45:23 <calamari> actually, left, so (t)r
19:45:30 <int-e> t(r), in the usual notation.
19:46:12 <int-e> that is, the idea is that t is a function and r is substituted for the first argument of that function
19:47:00 <int-e> as can be seen in the eta-reduction rule, (lx.t)r = t[x:=r]. (lx.t)r is a function application built of the function (lx.t) and the argument r.
19:59:58 <jix> Ka => lb.a ?
20:00:05 <int-e> yes
20:00:10 <jix> ok
20:03:51 <int-e> there's an additional complication - (lxy.xy)y is not ly.yy. instead you have to rename the variable in the lambda first (that's called a bound variable), for example to z - (lxz.xz)y and then apply alpha-reduction, to obtain lz.yz. This renaming of bound variables is called beta-conversion.
20:04:10 <int-e> forget all I said about eta-reduction, I don't know where my head was then - it's alpha-reduction.
20:04:27 <jix> SKKa => Ka(Ka) => a?
20:04:30 <int-e> eta-reduction is the rule lx.tx = t.
20:04:49 <int-e> yes.
20:04:53 <int-e> so, SKK=I
20:04:58 <jix> oh
20:05:04 <jix> s/oh/ok/
20:05:07 <int-e> because SKKa = Ia = a
20:06:00 <jix> what letter is η ?
20:06:27 <int-e> I is lx.x
20:07:21 <int-e> hmm. maybe we should use \ for lambda like the Haskell folks.
20:07:41 <jix> what about λ?
20:07:46 <cpressey_> or ^
20:07:55 <calamari> λ works :)
20:08:03 <int-e> no it doesn't
20:08:13 <jix> int-e: /charset utf8 (in xchat)
20:08:18 -!- cpressey_ has changed nick to cpressey.
20:08:36 <int-e> then I won't understand the other half of my chat partners
20:08:38 <int-e> ;)
20:08:57 <calamari> hi Chris
20:09:15 <calamari> \ is fine
20:09:27 <jix> int-e: you are from germany?
20:09:32 <int-e> jix, yes
20:09:36 * jix too
20:10:01 <jix> but do you speak german on freenode?
20:10:14 <jix> because in xchat charsets are network-lokal
20:10:23 <int-e> hmm. no I don't
20:10:31 <jix> but \ is easier to type
20:10:55 <int-e> äöü
20:10:57 * int-e thinks
20:11:12 <jix> &uuml; => ü
20:11:34 -!- Wrrrtbt has joined.
20:11:46 <Wrrrtbt> äöü
20:11:58 <int-e> äöü
20:12:05 <jix> äöü
20:12:21 -!- int-e has quit ("Bye!").
20:12:24 -!- Wrrrtbt has changed nick to int-e.
20:12:47 <int-e> seems to be better now
20:13:24 <int-e> thanks jix
20:13:43 <calamari> äöü
20:13:49 <jix> ß
20:14:07 <calamari> äöü = ß ?
20:14:11 <jix> no
20:14:12 <int-e> no
20:14:21 <calamari> I didn't change my term until after you guys did
20:14:26 <int-e> ß is the s-z ligature
20:14:28 <calamari>  λ
20:14:32 <int-e> &szlig;
20:14:41 <jix> fl &fllig;
20:14:46 <jix> :p
20:14:54 <int-e> scary
20:15:09 <jix> Å“ &oelig; ?
20:15:10 <calamari> &ffllig; ? 
20:15:16 <jix> hah oelig => ölig *g*
20:15:19 <calamari> how about &filig; ?
20:15:35 <jix> hmm
20:15:42 * int-e wonders which font xchat took that fl ligature from
20:16:03 <jix> there is no &filig; in html
20:16:07 <calamari> how did you produce it ?
20:16:11 -!- lindi- has quit (Remote closed the connection).
20:16:12 -!- lindi- has joined.
20:16:16 <jix> fllig?
20:16:17 <int-e> is there an ffllig?
20:16:21 <jix> alt-shift-l
20:16:29 <jix> int-e: not in html
20:16:39 <jix> alt-shift-l on a mac-de keyboard is fllig
20:16:42 <calamari> oic
20:16:57 <jix> ok back to λ
20:17:01 <calamari> heheh
20:17:09 <jix> church integers...
20:17:27 <jix> zero is λsz.z ?
20:17:36 <int-e> that lambda looks awful, too.
20:17:37 <int-e> yes
20:17:41 <calamari> barendregt numbers
20:17:52 -!- speedboy has left (?).
20:17:52 <int-e> although I prefer \fx.x
20:18:04 <int-e> f for function, x for argument
20:18:13 <calamari> \x.x
20:18:27 <jix> and one is one is *LAMBDA!!!!OMG!!!*sz.sz ?
20:18:56 <int-e> yes
20:19:00 <jix> hmm ' ' as lambda *g*
20:19:06 <int-e> and two is \fx.f(fx)
20:19:22 <int-e> and succ is \afx.f(afx)
20:19:25 * calamari needs to ignore and understand that first stuff first .. hehe
20:19:52 <int-e> and add is \abfx.af(bfx)
20:19:53 <jix> ok need to understand succ
20:19:54 <int-e> and so on
20:22:47 <jix> SUCC ONE => (\afx.f(afx))(\sz.sz) => \fx.f((\sz.sz)fx) => \fx.f(fx) ... ok works
20:23:08 <int-e> hmm. mul is \abf.a(bf)
20:23:38 <jix> mul is replacing the f of one number with the other number right?
20:23:47 <int-e> basically
20:24:12 <jix> i thought i'd never understand lambda-calculus...
20:27:55 <calamari> int-e: so in your Sabc example WAY up there you are going left to right?  I assume this means parethesis are ignored in favor of left associative?
20:28:00 <int-e> booleans are funny, too. true is \xy.x, false is \xy.y. if is \xyz.xyz (or just \x.x). a test for zero is \n.n(\x.false)true = \n.n(\xyz.z)(\xy.x)
20:28:58 <int-e> no, the parentheses are not ignored at all
20:29:06 <calamari> otherwise, I'd think the \z would be converted first rather than \x
20:29:18 <calamari> since it is more deeply nested in parenthesis
20:29:27 <int-e> I need to find a subterm of the form (\x.t)r to apply alpha-reduction.
20:29:53 <calamari> does alpha reduction actually reduce anything?  seems like it just rewrites
20:30:19 <int-e> well, that depends
20:30:21 <jix> (\abc.acb)(\xy.x) => (\bc.(\xy.x)cb) => (\bc.c) so \abc.acb is NOT?
20:30:30 <int-e> in its simple form it reduces the number of lambdas left
20:30:48 <int-e> yes
20:30:52 <jix> hah cool
20:31:02 <calamari> because I wouldn't know what to do with t[x:=r].. seems useless
20:31:14 <jix> hmm ok i'm trying to write a xor
20:31:48 <calamari> perhaps I should ignore alpha reduction and just use beta and eta?
20:32:25 <int-e> calamari no
20:32:41 <int-e> alpha reduction is the core of the lambda calculus
20:33:26 <int-e> it wouldn't be interesting without it - you wouldn't be able to do all those computations with it that make it turing complete.
20:33:32 <jix> hmm is \abtf.a(bft)b xor?
20:34:03 <int-e> hmm. no, you need (btf) at the end
20:34:28 <jix> yes?
20:34:41 <int-e> \abtf.a(bft)(btf)
20:34:48 <jix> oh yes...
20:34:55 <calamari> ((((lx.(ly.(lz.((xz)(yz)))))a)b)c) = (((ly.(lz.((az)(yz))))b)c), why is lx removed and not lz?  that's what's confusing me
20:35:08 <int-e> alternatively, you can use \a.a(not)(id) = \a.a(\xyz.xzy)(\x.x)
20:35:32 <int-e> I reduce the subterm ((lx.(ly.(lz.((xz)(yz)))))a)
20:35:55 <int-e> which is of the form ((lx.some term)a)
20:36:26 <int-e> there is no subterm of the form ((lz.some term)some other term), so I can't reduce the lz at that point
20:37:23 <int-e> the line starting with 'alternatively' was for jix
20:37:43 <calamari> yeah :)
20:38:41 <jix> and: (\a.a ID (K FALSE))?
20:39:06 <int-e> is and
20:39:16 <jix> yes i said 'and:' ;)
20:39:20 <int-e> oh
20:39:28 <jix> hah that's cool
20:39:47 <jix> hmm what about digital church like numbers
20:40:37 <calamari> maybe I need to start simpler
20:40:38 <jix> church numbers are base 1 (all "digits" count 1)... what about base 2..
20:41:32 <int-e> there are a few ways to build lists ...
20:44:48 <int-e> nil = \f.f false. cons = \a l.\f.f true a l   would work, for example. [nilp = \l.l(\t.t(\xy.false)true), etc]
20:45:36 <calamari> (lx.x)a = a
20:45:52 <int-e> calamari: yes
20:45:54 <calamari> or I should get used to (\x.x)a = a
20:46:18 <calamari> yay.. getting things started then :) 
20:49:38 <calamari> (\x.(\y.xy)a)b = (\x.xa)b ? 
20:52:06 <int-e> yes
20:52:36 <int-e> = ((\y.by)a) (two different alpha-reductions possible)
20:53:23 <calamari> so it is ambiguous?
20:56:28 <int-e> well yes
20:57:06 <int-e> but it's confluent - if a term reduces to two different terms, it's possible to reduce those terms to the same term again.
20:57:39 <calamari> (\y.by)a = b   (by eta) ?
20:58:08 <calamari> and (\x.xa)b = b by that eating rule
20:58:23 <int-e> no, (\y.by)=b (by eta), so (\y.by)a = ba
20:58:44 <int-e> and (\x.xa)b = ba by alpha-reduction
20:59:05 <calamari> hmmm
20:59:16 <calamari> \x.tx=t ?
20:59:21 <int-e> yes
20:59:36 <int-e> as long as t does not contain x. obviously
21:00:08 <calamari> oh.. I see my error
21:02:10 <calamari> is there a simpler case of alpha reduction?  I do not understand (\x.xa)b = ba
21:02:43 <calamari> or is that just the simplest case?
21:02:48 <jix> it's simple
21:03:52 * calamari adds it to his list of rules
21:03:55 <int-e> the simplest case is (\x.x)a = a.
21:04:54 <int-e> but what you actually do there is that you take the term 'x' (the right side of \x.x) and replace every occurence of x (that's the letter on the left side of \x.x) by a (that's the term following the (\x.x))
21:05:12 <jix> lambda rules!
21:06:05 <calamari> int-e: ahh, cool
21:06:08 <calamari> thanks
21:09:51 <jix> hmm i'll try to do a -1
21:10:12 <jix> that's not as easy as +1/SUCC
21:10:33 <int-e> you can make a function that maps 0 to 0 and every other number n to n-1
21:10:49 <int-e> and it is an interesting task indeed.
21:13:02 <calamari> Ka = (\xy.x)a = (\x.(\y.x))a = \y.a
21:13:58 <int-e> yes
21:14:38 <calamari> just to make sure \abcdef.g=g?
21:14:49 <int-e> no
21:14:51 <calamari> ok
21:15:14 <int-e> (\abcdef.g)xxxxxx = g
21:16:06 <calamari> oh right.. need some inputs there :)
21:26:48 <calamari> KK = (\xy.x)(\xy.x) = (\x.(\y.x))(\x.(\y.x)) = \y.(\x.(\y.x)), as above no prob
21:30:27 <calamari> SS = (\xyz.xz(yz))(\xyz.xz(yz)) = (\x.(\y.(\z.xz(yz))))(\x.(\y.(\z.xz(yz)))) = \y.(\z.(\x.(\y.(\z.xz(yz))))z(yz)) 
21:31:08 <calamari> coolness. I think I have alpha reduction down.. took me long enough :)
21:33:02 <calamari> that \xy expansion comes in very handy.. thanks for that 
21:35:21 <jix> KK is wrong...
21:35:24 <jix> KK = (\xy.x)(\xy.x) = (\x.(\y.x))(\x.(\y.x)) now you have to rename one of the K terms (\x.(\y.x))(\a.(\b.a)) = \b.(\x.(\y.x))
21:35:42 <int-e> no KK is right.
21:36:07 <jix> you can reuse y?
21:36:11 <jix> in one term?
21:36:16 <int-e> yes
21:36:27 <jix> oh you can use it because it isn't used inside...
21:36:35 <int-e> you just have to be careful with unbound occurences of a variable
21:39:40 <int-e> basically \x.t introduces its own scope for the variable x - namely the term t. you have to be careful when alpha reduction would change the scope of a variable as in (\xy.xy)y where a globally scoped y would become locally scoped in \y.yy.
21:39:51 <int-e> in that case you need to rename the inner variable.
21:39:56 <jix> k
21:40:02 <int-e> none of that happens in the KK example
21:40:47 <jix> if i have a x and a (\x. bla) in the same scope.. i can't use the outer x in the bla code right?
21:41:10 <int-e> right, that would be shadowed
21:41:14 <jix> and if i want to use it i have to rename the inner x to something different
21:41:29 <int-e> to reuse programming language vocabulary (as I did with scoped)
21:41:37 <int-e> right
21:48:34 <calamari> (\x.x(\x.y))a = x(\a.y) ?
21:48:59 <jix> a(\x.y)
21:49:33 <jix> maybe thinking of (\x.x(\x.y))a => (\.a(\x.y))a => a(\x.y) helps
21:50:48 <calamari> \.a? 
21:51:20 <jix> yes you remove the x from the left side of the . and replace it on the right side
21:51:45 -!- Keymaker has joined.
21:52:00 <jix> then the left side is empty.. well if it's empty there is no lambda so you can remove it
21:52:02 <Keymaker> greetings.
21:52:07 <jix> if it confuses you just ignore it
21:52:08 <jix> moin Keymaker 
21:52:15 <Keymaker> moin
21:52:27 <Keymaker> i've got couple of interesting ideas
21:52:51 <Keymaker> (note: they'll be revealed if ever ready)
21:54:34 <calamari> hmm yeah it'd be a(\a.y) in my original anyways
21:54:57 <calamari> but I guess \x stays unchanged
21:57:37 <calamari> does that seem right ?
21:58:08 <calamari> \var is not modified by alpha ?
21:59:49 <calamari> if so, Iota i = \x.xSK = \x.x(\xyz.xz(yz))(\xy.x) = \x.x(\x.(\y.(\z.xz(yz))))(\x.(\y.x)) = (\x.(\y.x))(\x.(\y.(\z.(\x.(\y.x))z(yz))))
22:00:26 <int-e> yes the \x stays unchanged
22:00:30 <calamari> don't want to go on if that is wrong tho :)
22:00:33 <calamari> oh, cool
22:00:35 <int-e> and also all x inside the \x
22:00:58 <calamari> can you give an example of that last thing?
22:01:16 <int-e> but I don't know what you did to that i
22:01:39 <int-e> (\xx.xx)a = \x.xx
22:01:41 <jix> (\x.x(\x.xy))a => a(\x.xy)  but (\x.x(\y.xy))a => a(\y.ay) right?
22:01:42 <calamari> it's an Iota i, defined as \x.xSK
22:02:10 <int-e> what did you do in the last step?
22:02:27 <calamari> int-e: I replaced x by (\x.(\y.x))
22:02:39 <int-e> you can't do that
22:03:01 <jix> thats saying I == K
22:03:17 <int-e> \x.xSK is \x.(xSK)
22:03:18 <calamari> int-e: it seems like a valid alpha 
22:03:40 <int-e> not (\x.xS)K as you interpreted it
22:03:48 <jix> oh i thought x == (\x.(\y.x))..
22:03:56 <jix> i thought you said...
22:03:58 <jix> nah
22:04:01 <jix> stupid me
22:04:10 <calamari> oic.. I thought it was left associative.. 
22:04:13 <jix> (\nxy.n (\abc.b(a c c)) (\ab.y) i x) << is this a PREV ?
22:04:26 <jix> and is there a lambda calculator?
22:05:11 <int-e> what's i?
22:05:18 <jix> oh should be I
22:05:18 <jix> ID
22:05:21 <int-e> ok
22:05:43 <jix> the PREV i saw was much longer and complicated
22:05:48 <jix> so i think i'm wrong
22:08:35 <int-e> I think it will fail on 2; you'll need to deal with real pairs
22:09:10 <int-e> pairs can be represented as pair := \abx.xab; with first = \a.a true and second = \a.a false.
22:11:00 <jix> hmm for me it works with 3
22:11:14 <int-e> maybe I'm missing something
22:11:50 <jix> but manual reduction isn't always 100% correct.. i need a program to reduce lambda expressions
22:12:16 <calamari> Iota i = \x.xSK = \x.(xSK) = \x.((xS)K) = \x.((x(\xyz.xz(yz)))(\xy.x)) 
22:12:44 <int-e> http://homepages.cwi.nl/~tromp/cl/cl.html
22:12:46 <calamari> but then I'm not sure I can reduce anything.. can I ?
22:12:58 <int-e> calamari, no you can't
22:15:29 <jix> int-e: the interpreter has only combinatory logic terms no way to enter lambda terms.. do i miss something?
22:16:19 <int-e> I missed that the Lambda calculus interpreter link on that page is broken :(
22:16:53 <int-e> http://ling.ucsd.edu/~barker/Lambda/
22:17:04 <int-e> seems to do
22:17:46 * int-e has his alphas and betas mixed up, too, apparently
22:17:48 * int-e sighs
22:17:53 <int-e> it's been too long.
22:17:59 * int-e shouldn't trust his memory
22:18:29 * calamari makes a quick eraser mark.. there fixed!
22:18:43 <calamari> thanks a lot for explaining this in detail 
22:19:20 <int-e> http://www.phost.de/~stefan/Files/ has a lambda interpreter, too
22:19:49 <int-e> i'm sure there are others
22:20:18 <int-e> jix, I think you're leaving out parentheses in your reductions for that PREV.
22:20:35 <jix> hmm
22:21:03 <jix> the first lambda interpreter has needs parantheses for every application
22:22:44 <jix> and the 2nd one refuses to compile.. redefines getchar...
22:22:49 <int-e> oh?
22:23:07 <jix> scanner.cc:67: error: new declaration 'char getchar()'
22:23:08 <jix> /usr/include/stdio.h:270: error: ambiguates old declaration 'int getchar()'
22:23:58 <int-e> yes I see that. interesting.
22:25:34 <int-e> predates namespaces, too.
22:29:03 <int-e> http://www.inf.tu-dresden.de/~bf3/lambda-2.8-my.zip
22:30:00 <int-e> hmm, your PREV works.
22:30:15 <int-e> funny
22:30:26 <int-e> don't know what I did wrong when I tried it.
22:31:46 <jix> cool
22:32:28 <int-e> there wasn't much to update in that program - I renamed getchar and ungetchar and added a bunch of using namespace std.
22:32:43 <jix> hmm i think if i show this to my friends they will think i'm crazy
22:32:57 <int-e> I'm still surprised Stefan used C library function's names there.
22:33:24 <int-e> (I know him personally)
22:33:29 <jix> ah
22:33:46 <int-e> but this was 1999
22:33:47 <int-e> hehe
22:34:17 <jix> is it possible to hack readline into the app?
22:34:31 <int-e> you might enjoy the standard library, it has an even shorter version of a predecessor function
22:34:33 <jix> i hate command lines without working cursor keys...
22:34:39 <int-e> (not much shorter though)
22:34:54 <int-e> I'm sure it's possible. I won't do it though.
22:35:13 <jix> and i don't know c++
22:35:34 <int-e> err actually
22:35:38 <int-e> it uses readline here
22:36:00 <jix> actually it doesn't find my readline... :(
22:37:32 <jix> ok it compiles with readline now
22:40:17 <jix> ok but i understand how the stdlib pred works
22:40:33 <jix> same idea as mine but nicer implementation
22:45:21 <int-e> some of these macros were created by me actually, we worked on them together.
22:49:09 <calamari> bbl.. 
22:49:18 -!- calamari has quit ("Leaving").
22:51:59 <jix> hmm the c++ lambda app is usefull for generating lazy-k code too
22:52:21 <jix> and it's even better for debugging it
22:53:19 <int-e> hehe
22:53:41 <int-e> hey, apparently that predecessor thingy was created by me, I even got credit :)
22:54:21 <jix> but it uses bruteforce for generating numbers... lazier uses <mul< 8 5 for 40... which is shorter than 40....
22:54:26 <int-e> it's also sort of useful for creating unlambda programs
22:54:44 <jix> lazy-k is better than unlambda
22:54:59 <jix> lazy-k has only s k and i...nothing else
22:56:27 <jix> ski <quicksort>      
22:56:27 <jix> Segmentation fault
22:56:28 <int-e> our favourite at the time was the power operator ... \x y.y x
22:56:57 <int-e> oh fun
22:57:53 <jix> maybe ski tries to expand the recursion..
22:57:59 <int-e> stack overflow
22:58:05 <jix> if it does it's useless for lazy-k
22:58:19 <jix> lazier has no problems with recursion
22:59:21 <int-e> lambda> ski (\x.x x x)(\x.x x x)
22:59:21 <int-e> (S (S I I) I (S (S I I) I))
22:59:21 <int-e> lambda> (\x.x x x)(\x.x x x)
22:59:21 <int-e> Auswertung abgebrochen nach 2733 Schritten.
22:59:24 <int-e> hmm
23:00:24 <int-e> quicksort is cheating
23:00:40 <int-e> it's working with recursive macro expansion
23:00:41 <jix> hm?
23:00:49 <jix> ah
23:01:00 <jix> that is cheating
23:03:57 <jix> greater than 0 test: (?n t f. n (?x.t) f)
23:04:45 <jix> and iszero if you swap t and f
23:05:22 <jix> and its shorter than the stdlib iszero
23:06:25 <int-e> ah, nice idea
23:14:16 <jix> i've an idea for a fast div by 2
23:14:34 <jix> oh and the stdlib div is cheating too...
23:15:03 <int-e> I know
23:15:11 <int-e> the list div in listop.la isn't though
23:20:44 <jix> it's slower than ndiv but it's shorter (only for div by 2
23:20:49 <jix> (?n x y.n (?a b c.b(a c b)) (?a b.y) (?x.x) x)
23:20:59 <jix> and it floors
23:21:31 <int-e> ndiv floors too
23:21:37 <jix> yes
23:21:55 <jix> (?n x y.n (?a b c.b(a c b)) (?a b.y) x (?x.x)) ceils
23:24:13 <int-e> ah. thanks, I know why I had trouble with understanding the PREV code now
23:24:34 <int-e> I was somehow thinking of numbers as fffffffx instead of f(f(f(f(fx))))) ...
23:24:46 <int-e> which makes no sense at all
23:24:57 -!- heatsink has joined.
23:25:40 <int-e> and that's slower than ndiv?
23:25:49 <int-e> interesting.
23:25:52 <jix> yes..
23:25:56 <jix> but it's shorter
23:26:09 <int-e> I'd exepect it to be faster actually
23:26:14 * jix too
23:27:33 <int-e> it'll be hard to create a generic div using that scheme though
23:28:03 <int-e> you'll probably end up with creating an infinite list of some sort, too - probably made of id and succ elements.
23:28:41 <jix> (?n x y.n (?a b.b(a (?z. b (x z)))) (?a.y) x) is sum of [0..n]
23:29:15 <jix> hmm i'm unnormal...
23:30:06 <jix> i don't now any other 14 years old person who has fun writing lambda terms....
23:31:34 <jix> (?n x y.n (?a b.b(a (?z. b (b z)))) (?a.y) x) is sum of [0,2^0..2^(n-1)]
23:32:03 <jix> which is 2^n-1
23:32:32 <int-e> hmm, ndiv is slower for me
23:32:59 <jix> i'm on ppc..
23:34:04 <int-e> your div2 needs fewer reductions
23:34:34 <jix> ppc function calls are faster than x86 ones...
23:34:43 <int-e> jix: \n.<pred> (n 2)
23:35:03 <jix> shorter-pipelines and intensive use of register-argument-passing
23:35:19 <int-e> right
23:35:19 <jix> (? x.<pred> (<pow> 2 x)) is faster than (?n x y.n (?a b.b(a (?z. b (b z)))) (?a.y) x)
23:36:45 <jix> is there a faster solution for (?n x y.n (?a b.b(a (?z. b (x z)))) (?a.y) x)?
23:39:23 <int-e> hmm, the formula would be n(n+1)/2 but the division by two kills it
23:42:20 <jix> (?n. <ndiv> (<mul> n (<succ> n)) 2) is slower even on ppc!
23:43:12 <jix> why is not (?x.x (?x y.y) (?x y.x))
23:43:29 <jix> and not (?x t f.x f t)
23:44:06 <int-e> because we didn't optimize that for some reason
23:44:11 <jix> hehe
23:45:43 <jix> <xor> is unoptimal too
23:45:56 <jix> lamba's xor: (?x y.x (y (?x y.y) (?x y.x)) y)
23:46:06 <jix> my xor: (?x.x (?x t f.x f t) (?x.x))
23:46:43 <int-e> I know.
23:48:15 <jix> is-dividable-by-two: (?n.n (?x t f.x f t) (?x y.x))
23:48:53 <int-e> yep
23:49:09 <int-e> and replace last x by y to get a check for odd numbers
23:49:15 <jix> hmm i need signed fractions...
23:49:22 <jix> ;)
23:51:52 <jix> would (?c x y.c sign nominator denominator) be possible?
23:52:10 <int-e> that's a triplet, yes
23:52:14 <jix> ok
23:52:21 <int-e> hmm
23:52:23 <int-e> actually
23:52:37 <jix> i'll start with multiplication..
23:52:39 <int-e> why not just (?s.s sign nominator denominator)
23:52:53 <jix> hmmm yes why not..
23:52:58 <int-e> with a selector s: \xyz.x for first, \xyz.y for second, \xyz.z for third component.
23:54:03 <jix> rational.la i'm ready
23:54:19 <int-e> fear!
23:59:21 <int-e> btw, lambda does understand \x for ?x if you prefer that. the ? was the original symbol though.