00:00:49 then it says that Q(y1,...,ym) = P(1,...,1) = 0 (mod p), hence Q(y1,...,ym) = +/- p is Q is constant and so is P 00:02:51 fax: what's the abstract algorithm for finite integrals? 00:02:53 maybe I can J it up 00:03:56 alise, I don't know what you mean.. symbolic antidifferentiation? 00:05:44 -!- coppro has joined. 00:06:02 for definite integral you can just sum up the values 00:06:04 because it's finite! 00:06:38 your sigma definition in al-jabr looked all higher order 00:07:10 I should do integrals as an adverb: so I get the derivative function, and two arguments 00:07:14 but that's all 00:08:21 oerjan: its linear time tho. 00:08:28 since you again dont have to _solve the linear equation 00:08:36 i did my math wrong before 00:08:38 Fixpoint Sigma n a f := 00:08:38 match n with 00:08:38 | O => 0 00:08:38 | S n => f a + Sigma n (a + 1) f 00:08:38 end. 00:08:38 Definition Discrete_Definite_Integral a b f := 00:08:39 match b - a with 00:08:39 | Zpos p => Sigma (nat_of_P p) a f 00:08:40 | _ => 0 00:08:40 end. 00:08:43 Is this just because Coq sucks at recursion? 00:08:46 (Sorry for the flood.) 00:08:57 With J it should be a cinch, since it is awesome at arrays. 00:09:03 What's a simpler general recursive definition? 00:09:14 essentially you can refactor the expression into a{6x}b{2y}c{5x-y-z} 00:09:15 I've no idea what nat_of_P is for starters. 00:09:21 Z -> N? 00:10:09 So a (f integ) b, we do b - a, if it's negative then 0, otherwise... 00:10:14 ? Sigma n recurses indefinitely. 00:10:22 That doesn't really work. 00:10:27 and so you just recognize 6x a's and, 2y b's, and for each, determine what x and y are, and if they're not integers, fail. 00:11:06 fax: is this some magic? 00:11:14 hm? 00:11:26 Sigma is that normal big-summation thing 00:11:48 augur: if you are right, it only means i was not clever enough with my example - it should be possible to find one where the original variables are _not_ determined by the string parsed 00:11:56 oh, it decomposes n into n 00:12:00 that's confusing, call it n' or something 00:12:20 oerjan: im not sure if that even makes any sense 00:12:23 which was my point with using more variables than equations in the first place 00:12:27 so Sigma n a f = sum (map (\_ -> f a) [0..n]) 00:12:36 0 to n inclusive? Yes. 00:12:40 no wait 00:12:42 it's ... hm 00:12:50 it's just multiplication fax 00:12:56 oh wait no it's not 00:13:01 because if the variables range over Z, and exponents range over Z, then obviously we can just refactor and if at any more one of them fails to do so, we're done 00:13:06 sum (map f [1..n]) 00:13:08 right? 00:13:10 we're still not _solving_ diophantines 00:13:24 also, holy fuck i have hand sanitizier that smells EXACTLY like pot 00:13:40 maybe it's actually pot that works like hand sanitiser 00:13:45 augur: the variables range over N 00:14:04 which should be obvious, since you don't have negative length string 00:14:05 *s 00:14:08 fax: Sigma n a f = sum (map f [1..n]) right? Just getting the range right 00:14:12 well, the exponents, at least. 00:14:27 i mean, theres no harm in ranging the variables over Z, so long as the exponents are always N 00:14:45 augur: my notation is simply meant as an abbreviation for expanding the sums out 00:15:13 alise yeah 00:15:14 e.g. if you had some expression a{m}b{n}c{m-n} and you tried to recognize abb..., you would calculate that you need 2-3 = -1 c's 00:15:21 which fails immediately because its a negative exponent 00:16:20 if. (y-x) > 0 do. +/ v (x+i. (y-x)) else. 0 end. 00:16:25 augur: the thing is that with sufficiently complicated linear equations, you can get into trouble determining whether any of the several solutions is a natural number. in fact even integers might give enough trouble. 00:17:25 -!- alise_ has joined. 00:17:25 but theres no harm in letting the variables range over Z, because itll just force things to be refactored. e.g. a{m}b{n}c{m-n} is just a{m+n}b{m}c{n} 00:17:33 fax: ok right gimme an example to test integ 00:17:43 oerjan: but these arent EQUATIONS 00:17:46 thats the point, right 00:18:00 they're really just sums 00:18:14 augur: i am talking about the equations i'm trying to turn into examples that show you that you cannot get away with not solving them :D 00:18:17 i mean, if you did lets say 00:18:59 fax: plz 00:19:18 if you had something like a{x^2 + y^2}b{x}c{y} 00:19:23 no even that 00:19:44 fax: so this is my understanding of integrate 00:19:47 your def 00:20:17 oerjan: im failing to see any situation where it actually _is_ a problem 00:20:30 integ f x y | y-x > 0 = sum (map f [(y-x)..(i-1)]) 00:20:32 | otherwise = 0 00:20:33 -!- alise has quit (Ping timeout: 240 seconds). 00:20:39 where [m..n] is [m,m+1,...,n-1,n] 00:20:43 fax: isthis right? 00:20:46 *is this 00:21:17 hello 00:22:31 23:20 integ f x y | y-x > 0 = sum (map f [(y-x)..(i-1)]) 00:22:31 23:20 | otherwise = 0 00:22:31 23:20 * alise (~alise@genld-216-213.t-mobile.co.uk) Quit (Ping timeout: 240 seconds) 00:22:31 23:20 where [m..n] is [m,m+1,...,n-1,n] 00:22:31 is that your def? 00:22:37 erm 00:22:51 23:20 integ f x y | y-x > 0 = sum (map f [x..(y-x)]) 00:22:52 23:20 | otherwise = 0 00:22:52 23:20 * alise (~alise@genld-216-213.t-mobile.co.uk) Quit (Ping timeout: 240 seconds) 00:22:52 23:20 where [m..n] is [m,m+1,...,n-1,n] 00:22:53 that's not right... 00:23:22 alise use the paper instead of my code! 00:23:23 ok so we loop (y-x) times, first value to the function is x 00:23:28 it's much clearer, and all my stuff is copying it exactly 00:23:30 fax: no :) 00:23:53 so 00:23:53 i.(y-x) 00:23:53 yields a list starting at 0 of (y-x) in length 00:23:53 x + i. (y-x) 00:23:53 ok, that's right 00:23:54 so then we u on it 00:23:54 and +/ 00:23:56 if. (y-x)>0 do. +/u x+i.y-x else. 0 end. 00:24:02 this is right, so why do i get domain errors 00:24:10 -!- cheater2 has quit (Ping timeout: 264 seconds). 00:24:13 ehh just gimme a dead simple example to test :)) 00:24:50 3 (id integ) 4 00:24:50 |domain error 00:24:50 | 3 (id integ)4 00:24:52 there is no damn reason for that 00:24:53 example of waht? 00:24:57 -!- cheater3 has joined. 00:24:58 your finite integ 00:25:17 augur: what about /a{256*x}a{3*y}b{y}b{256*z}/ 00:25:18 what's going on? 00:25:31 ok seriously my definition is right 00:25:33 myabe the if is the problem 00:25:49 oejan, what about it? 00:25:49 (trying to find an example based on the brainfuck constant algorithm trickeries 00:25:50 nope 00:25:53 ) 00:26:03 augur: can you refactor that? 00:26:12 recognize some number of a's, divide by 256, if thats not an int, fail 00:26:16 oh i see 00:26:19 oh my lets see :x 00:26:41 "integ f x y | y-x > 0 = sum (map f [x..(y-x)])" <<< you go from x to y-x? so y's like 2x+offset? 00:26:49 i mean not that i have any idea what that's about 00:27:57 finite integration 00:28:01 my j definition is breaking 00:28:02 fix it :) 00:28:23 integ =: adverb define 00:28:24 if. (y-x)>0 do. +/u x+i.y-x else. 0 end. 00:28:24 ) 00:30:00 oerjan, first, w must be a multiple of 3 00:30:05 ew 00:30:08 er 00:30:15 the number of a's must be a multiple of 3 00:30:23 augur: incorrect 00:30:27 no, correct 00:30:32 no, incorrect 00:30:32 * fax downloads j 00:30:36 oerjan 00:30:48 it is correct 00:30:51 and let me prove to you why 00:30:52 256 is not divisible by 3 00:30:57 fax: good idea, watch out for the installer it fucks your home directory (ok well adds a directory or two to it) 00:31:01 that is irrelevant to the point 00:31:06 you can specify a different dir but make sure you can write in it 00:31:06 x is not used anywhere else 00:31:08 alise_: how do you apply an adverb? :P 00:31:12 be quiet, oerjan 00:31:13 and listen 00:31:38 augur: no it is not, you can add 256 a's to any solution and get a new one, which is not a multiple of 3 if the original is 00:31:44 a^(256x + 3y) b^(y + 256x) = a^w b^(w/3 - 256x - 256w) 00:31:58 * fax realizes how much I have forgotten when given a blank window 00:32:15 er, 256x/3 00:32:15 -!- MizardX has quit (Read error: Connection reset by peer). 00:32:27 - 256z 00:32:28 -!- MizardX has joined. 00:32:28 not w 00:32:29 sorry. 00:32:57 alise_: how do i apply that to a function and two data arguments? 00:33:11 a^w b^(w/3 - 256x/3 - 256z) 00:33:20 i can't just do "x function integ y" 00:33:23 oklopol: x (func integ) y 00:33:27 oh. 00:33:27 produces a domain error, helpfully 00:33:29 i can huh 00:33:33 no matter what you plug in 00:33:43 ah okay, is that the problem? 00:33:53 oklopol: lol 00:33:53 its just like x +/ y 00:33:53 *it's 00:33:53 here's its pal deriv 00:33:53 deriv =: adverb define 00:33:54 u (y+1) - u y 00:33:54 ) 00:33:55 that one actually works 00:34:07 well you might be right actually :) 00:34:18 * oerjan cackles evilly 00:34:19 oklopol: what that integ produces a domain error all the time? 00:34:28 yes. i don't think the algorithm-if-it-worked has been translated incorrectly 00:34:41 alise_: i thought there had to be special syntax for when it's letters and not operator letters, exactly because it produced a domain error 00:34:52 well, (foo deriv) x works so 00:34:55 then again why would that give me a domain error 00:34:59 well exactly 00:35:10 j comes with a debugger, I think i'll try that 00:35:24 fucking hell what's the identity 00:35:40 if i can find it lol 00:36:23 id v 3 : (,'y') 00:36:29 that is ... not helpful 00:36:43 ah what the FUCK 00:36:57 -!- cheater3 has quit (Ping timeout: 276 seconds). 00:36:57 id =: monad : 'x' -- this is wrong 00:37:01 id =: monad : 'y' -- this works 00:37:08 ? 00:37:10 yeah 00:37:11 because 00:37:14 (x u y) 00:37:15 is application 00:37:19 ??? 00:37:20 so (u y) is just a simplified form of that 00:37:22 oh 00:37:30 remember everything is infix even things that aren't :)) 00:37:41 also often this is a nicer syntax for definitions: 00:37:45 id =: monad define 00:37:45 y 00:37:45 ) 00:37:50 longer ones anyway 00:38:01 -!- cheater2 has joined. 00:38:04 specially ones with strings :) 00:38:10 oerjan, so if we accept that this might be tricky, how can we make it trivial 00:38:15 oklopol: you might be right about needing special syntax for the dyadic adverb case 00:38:18 eliminating addition would do it 00:38:34 atleast, variable addition 00:38:53 so a{2x+3} is fine, but a{2x+y} is not 00:38:54 a hint is it doesn't work no matter what the code in the body is 00:38:55 alise? +/ f a + i. b 00:38:58 this seems to work 00:39:00 Unlike verbs, adverbs and conjunctions have fixed valence: an adverb is monadic (applying to a single argument to its left), and a conjunction is dyadic. 00:39:02 the call gives a domain error 00:39:02 ahh 00:39:05 maybe i need a conjunction! 00:39:11 augur: so each character can only be used with one variable? 00:39:15 sum f mapped over the range a to b 00:39:23 yeppp i need a conjunction i think 00:40:05 3 (id integ) 4 00:40:05 |ill-formed name: ? 00:40:05 | ({."1 wdq) =:wd_val 00:40:05 wat. 00:40:07 oerjan, well, no that would be stupid 00:40:08 augur: after all you'll also have to disallow a{2x}a{y} 00:40:08 you're right 00:40:17 alise_: why conjunction? it just takes one verb 00:40:23 one function 00:40:25 ah right 00:40:28 then wtf is up :) 00:40:47 well dunno, do adverbs actually get to talk about the parameters the resulting verb is called with? 00:40:52 x and y 00:40:58 well, but oerjan, here's the good thing at least, right 00:41:01 i mean, i don't actually remember pretty much any syntax... 00:41:06 oerjan did you se the proof about primes? 00:41:09 yes they do 00:41:11 that's why deriv works :-) 00:41:15 hmm right 00:41:17 a^256x a^3y b^y b^256z is surely linear time, right 00:41:20 I just wrote the one from the book out 00:41:29 fax: the one with P(1,1,...,1) ? yes 00:41:51 okay 00:41:53 thats just (a...)^x (aaa)^y b^y (b...)^z 00:42:38 which would have minimal amounts of backtracking 00:43:45 http://www.mail-archive.com/general@jsoftware.com/msg04062.html 00:43:48 may be a monadic/dyadic issue??? 00:43:52 alise_: if it's any consolation, your deriv is wrong 00:44:00 hi oklopol 00:44:04 hi faxie 00:44:13 so if we didnt solve the simple diophantines, but instead had some amount of backtracking, it wouldnt be _too_ bad i think 00:44:16 (id integ) 4 00:44:16 |value error: x 00:44:16 | +/u x+i.y- x 00:44:20 well that's at least helpful 00:44:22 augur: mind you the diophantine equation in that particular case is not _that_ hard to solve. in fact i think several optimizing brainfuck compilers do it :D 00:44:26 oklopol, do you know about this bijection between N^2 and N! 00:44:36 (in essence) 00:44:38 well yes 00:44:44 f(x,y) = (x^2+y^2+x+2xy+3y)/2 00:44:51 oh well maybe not that one 00:44:55 it's so beautiful 00:44:56 oerjan: right, im just saying we dont have to solve them we could ust do something else 00:45:01 oerjan proved it in like 1 second 00:46:05 augur: i think if there is more than two variables for a given char, your backtracking could easily be quadratic etc. 00:46:09 *are 00:46:09 oh he did now 00:46:18 "Mathematical fields always permit further division." 00:46:22 and I didn't know that C(n,k) is the n'th k-dimensional pyramid 00:46:30 oklopol: mind you i guessed it was a basic idea i already knew about 00:46:37 oerjan: hm. ok so then we dont have linear time 00:46:45 so how do you prove it? 00:46:48 im partially ok with that, actually 00:46:52 My wit i sunmatched. 00:46:57 i mean one second sort of implies it's not some boring algebra 00:47:06 *is unmatched 00:47:19 im more interested in the class of languages that is representable in such a simple fashion 00:47:24 the parse complexity isnt a huge issue 00:47:32 fax: i didn't know that either, n'th as in of height n? 00:47:39 n'th in the sequence 00:47:54 for example nC2 = n(n-1)/2 triangular numbers 00:47:58 tho the linear time subset of those is itself interesting 00:48:06 oklopol: FIX IT :| 00:48:09 "in the sequence"? 00:48:13 alise_: fix what? 00:48:16 1,3,6,10,15,... 00:48:18 the derivative is trivial to fix 00:48:26 the deriv isn't broken. 00:48:29 oh well i see 00:48:33 oklopol, the really amazing bit is that the the FINITE INTEGRAL of nCk is nCk+1 00:49:01 (which explains why it's a bijection) 00:49:02 yeah finite integration and falling powers are pals 00:49:07 oh 00:49:29 and this generalizes too 00:49:38 so wait what do we see why f is a bijection now? 00:49:42 i don't see. 00:49:43 ` =: adverb : 'u (y+1) - u y' NB. now I just need a fancy symbol for my broken integration 00:49:44 No output. 00:49:53 oklopol, well if we are at T(3) = 6, 00:50:02 we can add 1, 2, or 3, until we hit T(4) 00:50:17 alise_: so what's ] deriv 1 00:50:27 2 - 1 = 1 00:50:30 so there is a bijection between N and (x,y) : NxN where y < x 00:51:26 oklopol: ] deriv 1 results in 1. why 00:51:28 oklopol: f(x,y) = (x+y)C2 + y iirc 00:51:39 it's exactly fax's def so... 00:52:12 aw ` isn't a valid name 00:52:38 alise_: oh sorry, ] doesn't show the problem 00:52:46 but try say +: deriv 6 00:53:02 and you can just shift it over to make the full bijection 00:53:06 skew 00:53:10 the derivative of +: is constant 2 00:53:41 oerjan: ah, okay that's cool 00:53:42 then fax's definition must suffer from the same problem 00:53:47 because his is exactly the same 00:53:51 where's fax's definition? 00:53:59 http://github.com/odge/al-jabr/blob/master/Fun/FiniteCalculus.v 00:54:01 are you sure she expressed it in j? 00:54:02 oerjan: on an unrelated note, wanna hear a cool technique for doing part-of-speech induction? :D 00:54:13 Definition DiscreteDerivative (f : Z -> Z) (x : Z) := f (x + 1) - f x. 00:54:20 okay 00:54:27 and you have f (x + 1 - f x) 00:54:30 XD 00:54:33 no i don't 00:54:40 hmm so i do 00:54:41 wow :D 00:54:45 well okay 00:54:46 pretty epic failure there 00:54:48 augur: not really, my head is on the verge of full 00:54:51 you have f ((x + 1) - f x) 00:54:53 aww 00:54:58 well empty some of it out! 00:55:00 i mean in j terms 00:55:10 anyway, im going to tell the channel anyway, oerjan 00:55:12 so dont worry :D 00:55:17 AAAAAA 00:55:19 oklopol! im going to tell this to you too 00:55:20 i mean, ok 00:55:28 8D 00:55:31 augur: go for it, not that i have any idea what's going on 00:55:31 deriv =: adverb : '(u y+1)-u y' 00:55:36 a nicer name would be... nice, though 00:55:49 +:` x etc 00:55:54 but that's not valid 00:55:54 oklopol: part of speech induction. that is, given some text in a language, discovering the parts of speech (noun, verb, etc.) 00:56:12 so the algorithm goes like this 00:56:17 http://www.jstor.org/pss/2323743 00:56:24 geometry of binomial coefficients - Stephen Wolfram 00:56:51 looking at the binary stuff :| 00:57:26 fax: yay, % deriv now produces a correct plot 00:58:01 + deriv still produces a ridiculous plot with little spikes at float errors 00:58:44 for each word, collect the "n-contexts" that it appears in, where the n-context of the word is the set of pairs of strings where each string is the n words immediately to the left/right of the word in some sentence the word appears in 00:59:03 nicee nice baby 00:59:25 e.g. if you have the sentence "the dog barked", the 1-context is (the, barked). if you have two sentenes, "the dog barked" and "the dog yelped", it has the 1-contexts {(the, barked), (the, yelped)} 00:59:54 so you just map each word to its sentential neighborhood, basically. 00:59:55 oklopol: now fix integ >_> 00:59:58 do you even know the error :P 01:00:26 then you build a graph where each node in the graph is a word, and an arc connects two words if the words share at least one context 01:01:12 that is, the graph is (V, E) where V is the words, and (w1, w2) is in E iff context(w1) intersect context(w2) is not empty 01:01:51 so that gives you a similarity graph, showing you which words show up in similar neighborhoods to which other words 01:02:16 then if you take the word-wise maximal cliques of this graph, you get the parts of speech 01:03:37 oklopol: I know the equation is correct - 01:03:41 +/] 3+i.1 01:03:41 3 01:03:47 it's just the definition is broken 01:03:56 and this algorithm works _surprisingly_ well 01:03:57 yeah but there's a domain error no matter what code you put in the if 01:04:05 augur: i'll read. 01:04:05 but its pretty slow. 01:04:17 at least with the maximal graph algos i have. 01:04:31 er, maximal clique. 01:05:13 oklopol: so it is the control structure. 01:05:45 ah 01:05:50 inside the ifneeds to be imperative things i think 01:05:52 *if needs 01:06:40 nope 01:06:45 augur: okay that does sound like an interesting idea 01:06:50 :) 01:06:58 i'll have to check the definition of maximum clique tho 01:07:04 i have a very vague idea 01:07:28 you know what a clique is right? 01:07:41 wait lol 01:07:43 The last sentence executed in a T block is tested for a non-zero value in its leading atom, determining whether the B block after the do. or the rest of the sentence is executed. An empty T block result or an omitted T block tests true. 01:07:43 or the rest of the sentence? 01:07:52 a clique is a complete subgraph 01:07:57 foo =: adverb define 01:07:57 y-x 01:07:57 ) 01:07:58 fails 01:08:06 that is, a subgraph where each vertex is connected to each other vertex 01:08:27 ywah 01:08:29 yeah 01:08:30 a maximAL (with an "al", not maximum "um") 01:08:32