00:16:51 [[Stupid]] M https://esolangs.org/w/index.php?diff=56850&oldid=56558 * Oerjan * (-27) rm nonexistent category 00:17:18 [[Stop]] M https://esolangs.org/w/index.php?diff=56851&oldid=56564 * Oerjan * (-27) rm nonexistent category 00:19:32 [[EsoScript]] M https://esolangs.org/w/index.php?diff=56852&oldid=56822 * Oerjan * (-4) fix category 00:19:50 [[Bit Stupid]] M https://esolangs.org/w/index.php?diff=56853&oldid=56562 * Oerjan * (-27) rm nonexistent category 00:20:29 [[Array Changer]] M https://esolangs.org/w/index.php?diff=56854&oldid=56244 * Oerjan * (-27) fix categories 00:36:11 -!- imode has joined. 01:13:49 -!- oerjan has quit (Quit: Nite). 01:19:05 -!- XorSwap has joined. 01:23:05 -!- pikhq has quit (Ping timeout: 240 seconds). 01:50:16 -!- tromp has joined. 01:54:27 -!- tromp has quit (Ping timeout: 240 seconds). 02:00:33 -!- Sgeo__ has quit (Quit: Leaving). 02:01:12 -!- Sgeo has joined. 02:06:08 -!- atslash has quit (Ping timeout: 255 seconds). 02:34:20 -!- pikhq has joined. 02:40:09 [[User:A]] https://esolangs.org/w/index.php?diff=56855&oldid=56847 * A * (-69) 02:43:27 -!- tromp has joined. 02:47:57 -!- tromp has quit (Ping timeout: 240 seconds). 02:49:27 [[Telegram]] https://esolangs.org/w/index.php?diff=56856&oldid=26665 * A * (+578) Unsure... 02:50:04 [[Telegram]] https://esolangs.org/w/index.php?diff=56857&oldid=56856 * A * (+7) Aw man...too messy! 02:53:23 [[User:A]] https://esolangs.org/w/index.php?diff=56858&oldid=56855 * A * (+15) 03:05:04 [[Talk:Logic]] N https://esolangs.org/w/index.php?oldid=56859 * A * (+162) Created page with "==Actually more shorter CAT program== I-| &-O 1-| That is a lot shorter. I think the CAT program in the page is user-unfriendly.--[[User:A]]11:04 19 Jul.2018" 03:05:55 [[Talk:Logic]] https://esolangs.org/w/index.php?diff=56860&oldid=56859 * A * (-5) Bad grammar. 03:34:16 -!- rdococ has quit (Changing host). 03:34:16 -!- rdococ has joined. 04:29:31 -!- tromp has joined. 04:34:35 -!- tromp has quit (Ping timeout: 276 seconds). 05:17:49 -!- XorSwap has quit (Ping timeout: 244 seconds). 05:18:49 -!- MDude has joined. 05:23:30 -!- tromp has joined. 05:27:45 -!- tromp has quit (Ping timeout: 245 seconds). 05:30:07 [[Shorten your Brainfuck code]] M https://esolangs.org/w/index.php?diff=56861&oldid=56721 * A * (+59) 05:30:32 -!- lynn_ has joined. 05:31:11 -!- lynn has quit (Ping timeout: 276 seconds). 05:31:14 -!- lynn_ has changed nick to lynn. 05:33:24 -!- lynn has changed nick to Guest55067. 06:01:52 -!- atslash has joined. 06:20:56 -!- tromp has joined. 06:25:27 -!- tromp has quit (Ping timeout: 240 seconds). 06:26:03 -!- moei has joined. 07:10:32 -!- tromp has joined. 07:14:50 -!- tromp has quit (Ping timeout: 255 seconds). 07:16:31 -!- aloril_ has quit (Ping timeout: 268 seconds). 07:17:26 -!- aloril_ has joined. 07:24:03 -!- tromp has joined. 07:46:12 -!- AnotherTest has joined. 07:46:35 -!- APic has quit (Ping timeout: 240 seconds). 08:38:43 -!- FreeFull has quit (Quit: Rebooting). 08:39:55 -!- FreeFull has joined. 09:02:20 -!- SopaXorzTaker has joined. 09:09:32 -!- imode has quit (Ping timeout: 276 seconds). 09:36:48 -!- SopaXT has joined. 09:37:07 -!- SopaXorzTaker has quit (Disconnected by services). 09:37:09 -!- SopaXT has changed nick to SopaXorzTaker. 09:38:46 -!- SopaXT has joined. 09:48:33 -!- SopaXT has quit (Ping timeout: 244 seconds). 10:13:30 [[Far]] https://esolangs.org/w/index.php?diff=56862&oldid=56530 * GibsonGeorge * (+60) 11:06:20 -!- SopaXorzTaker has quit (Remote host closed the connection). 11:06:52 -!- SopaXorzTaker has joined. 11:13:26 -!- lldd_ has joined. 11:33:12 -!- APic has joined. 12:21:56 -!- moei has quit (Ping timeout: 276 seconds). 13:06:08 [[Surtic]] M https://esolangs.org/w/index.php?diff=56863&oldid=56624 * Digital Hunter * (+41) /* S */ 13:24:00 -!- fungot has quit (Ping timeout: 256 seconds). 13:24:16 -!- fungot has joined. 14:22:53 -!- aloril_ has quit (Remote host closed the connection). 14:37:23 -!- aloril has joined. 14:40:24 -!- oerjan has joined. 14:54:41 -!- aloril has quit (Remote host closed the connection). 15:00:32 -!- aloril has joined. 15:33:41 -!- AnotherTest has quit (Ping timeout: 244 seconds). 15:34:31 -!- XorSwap has joined. 15:38:19 -!- PinealGlandOptic has joined. 15:54:58 -!- PinealGlandOptic has quit (Quit: leaving). 15:55:43 -!- yurichev has joined. 16:09:34 -!- oerjan has quit (Quit: Later). 16:20:42 -!- XorSwap has quit (Ping timeout: 244 seconds). 16:23:15 -!- erkin has joined. 16:33:01 -!- AnotherTest has joined. 16:36:46 -!- SopaXorzTaker has quit (Quit: Leaving). 17:07:30 -!- XorSwap has joined. 17:16:35 -!- deltab has quit (Ping timeout: 256 seconds). 17:34:09 -!- erkin has quit (Quit: Ouch! Got SIGIRL, dying...). 17:50:41 -!- deltab has joined. 17:56:56 -!- LKoen has joined. 18:02:08 -!- Phantom_Hoover has joined. 18:04:39 -!- imode has joined. 18:12:06 [[User:TuxCrafting]] https://esolangs.org/w/index.php?diff=56864&oldid=48916 * TuxCrafting * (+27) 18:12:07 -!- erkin has joined. 18:14:50 -!- tromp has quit (Ping timeout: 256 seconds). 18:15:39 -!- XorSwap has quit (Ping timeout: 260 seconds). 18:22:05 -!- Lean1 has joined. 18:24:43 -!- Lean1 has quit (Read error: Connection reset by peer). 18:25:52 -!- erkin has quit (Quit: Ouch! Got SIGIRL, dying...). 18:28:41 -!- Lean1 has joined. 18:29:19 -!- erkin has joined. 18:30:27 Why lemons? 18:30:50 those lemon whores! 18:31:53 yes they arid but? 18:35:51 -!- Lean1 has left. 19:20:06 -!- S_Gautam has quit (Quit: Connection closed for inactivity). 19:20:36 -!- yurichev has quit (Quit: leaving). 19:23:51 `olist 1128 19:23:52 olist 1128: shachaf oerjan Sgeo FireFly boily nortti b_jonas 19:30:20 -!- nchambers has changed nick to uplime. 19:39:43 [[User:DMC]] M https://esolangs.org/w/index.php?diff=56865&oldid=56784 * DMC * (-78) 19:55:14 -!- lldd_ has quit (Quit: Leaving). 20:09:44 -!- atslash has quit (Ping timeout: 255 seconds). 20:10:23 -!- MDead has joined. 20:11:25 -!- moei has joined. 20:11:44 -!- MDude has quit (Ping timeout: 260 seconds). 20:11:48 -!- MDead has changed nick to MDude. 20:13:42 -!- atslash has joined. 20:29:09 -!- MDude has quit (Ping timeout: 264 seconds). 21:03:01 -!- ais523 has joined. 21:04:27 -!- ais523 has quit (Remote host closed the connection). 21:04:40 -!- ais523 has joined. 21:09:07 -!- erkin has quit (Quit: Ouch! Got SIGIRL, dying...). 21:09:25 -!- LKoen has quit (Quit: “It’s only logical. First you learn to talk, then you learn to think. Too bad it’s not the other way round.”). 21:10:15 -!- tromp has joined. 21:18:19 -!- subleq has joined. 21:18:45 Are there any formal languages that do not always halt, but have a decideable halting problem? 21:19:12 it's fairly easy to create one 21:19:27 but finite state automata with halt states are the most obvious example 21:19:39 any infinite loop in those is detectable, so you can just run them until they halt or enter an infinite loop 21:20:17 I think even with PDAs, all infinite loops are detectable, but I'm less sure on that 21:28:49 you'll see the same state with the same stack iff it doesn't terminate i think 21:29:23 not necessarily the same, but the stack will form a repeating pattern 21:29:31 hmm 21:29:40 so you can see that the loop only looks at, say, the top 10 stack elements before repeating 21:29:54 and after that point the top 10 elements are the same, even if they might be at a different position on the stack 21:30:01 right 21:32:40 are there any programming languages equivalent to a PDA? 21:32:50 plenty 21:33:34 like? 21:33:35 [[Esolang:Categorization]] https://esolangs.org/w/index.php?diff=56866&oldid=56573 * Ais523 * (+35) /* Computational class */ add the PDA category to the list; we've been using it for years 21:33:46 here: https://esolangs.org/wiki/Category:Push-down_automata 21:33:54 Befunge-93 is probably the best known 21:34:56 [[Funge-98]] M https://esolangs.org/w/index.php?diff=56867&oldid=53358 * Ais523 * (-33) not a PDA; the existence of the stack stack (together with a swap instruction) gives it more storage than that 21:36:27 -!- ais523 has quit (Remote host closed the connection). 21:36:39 -!- ais523 has joined. 21:37:14 are you aware of any restrictions on lambda calculus that could work? 21:38:19 it's a bit complex, but "all arguments to a recursive or indirectly recursive call must be constants" works 21:38:30 i guess just adding a loop primative 21:38:34 or https://esolangs.org/wiki/Splinter is pretty similar 21:38:42 to a strongly normalizing lambda calculus would work 21:39:14 typed lambda calculus + tail-recursion (the closest lambda calculus equivalent to a while loop) is probably TC, I'm not 100% sure on that though 21:47:53 i mean something like this https://github.com/edwinb/TypeDD-Samples/blob/master/Chapter11/RunIO.idr 21:50:33 actually I'm not certain that any given type in typed lambda calculus has infinitely many functions of that type… 21:51:19 what? 21:52:24 like, if there are only finitely many functions of each type 21:52:39 then typed lambda calculus + tail-recursion would be a finite state machine, as there's a limited amount of state in the system 21:54:53 come to think of it, i'm not sure this is an interesting question, unless decidable halting languages are in a different class than always halting 21:55:52 -!- MDude has joined. 21:57:10 well, you can normally define "provably not halting" as a form of halting all of its own 21:57:30 because if you can prove it doesn't halt, now you know the eventual fate of the program 21:57:34 hah! 21:57:42 from that point of view, decidably-halting and always-halting aren't very different 21:57:52 indeed 22:05:45 [[]] https://esolangs.org/w/index.php?diff=56868&oldid=56787 * Fogity * (-1300) Now refers to the official documentation instead of trying to summarise the language details. 22:13:30 subleq: https://mathoverflow.net/questions/261934/is-simply-typed-lambda-calculus-with-fixed-point-combinator-turing-complete (first answer) is a fun one. 22:14:05 -!- AnotherTest has quit (Ping timeout: 276 seconds). 22:17:22 hmm, that paper is not publically available 22:17:26 subleq: oh yes, it's obviously TC if you add integers + basic operations on them (like increment, decrement, zero-test) 22:17:55 i don't get it, why aren't church numerals equivalent to primitive integers? 22:18:11 subleq: the types get increasingly complex as the numbers get larger 22:18:27 so they work fine in untyped lambda calculus, but in typed lambda calculus, any given type has a maximum Church number it can handle 22:18:35 oh 22:18:51 that is, unless you constrain the church numerals to acting on functions of a particular simplified type, but then you can't combine them with each other 22:21:27 hmm, I wonder if this invalidates the TCness proof for (=); Haskell 22:21:37 or if those characters are enough for TCness some other way 22:23:06 > let (===)==(====)=(===) in 0==3 22:23:08 0 22:24:16 so stlc with fix is not turing complete, but seemingly system f with fix is 22:25:42 Yeah, System F has proper Church numerals. (of type forall a. (a -> a) -> a -> a) 22:26:35 right, I was just coming to that conclusion myself, Haskell isn't actually simply typed so it may work by using polymorphism 22:27:15 > let two : (x -> x) -> (x -> x) = \ a b -> a (a b) in two (+1) 0 22:27:16 yeah but it's not System F, just Hindley-Milner... so (as far as I'm concerned) it needs some thought. 22:27:17 :1:20: error: parse error on input ‘->’ 22:27:28 > let two : (x -> x) -> (x -> x) = \ a b => a (a b) in two (+1) 0 22:27:29 :1:20: error: parse error on input ‘->’ 22:27:40 > let two : ((x -> x) -> (x -> x)) = \ a b -> a (a b) in two (+1) 0 22:27:42 error: 22:27:42 Pattern syntax in expression context: x -> x 22:27:44 it's :: 22:27:48 > let two :: ((x -> x) -> (x -> x)) = \ a b -> a (a b) in two (+1) 0 22:27:50 error: 22:27:50 • You cannot bind scoped type variable ‘x’ 22:27:50 in a pattern binding signature 22:28:00 I don't actually know Haskell syntax 22:28:08 also I thought :: was lists 22:28:13 let a = 4::[] in a 22:28:16 > let a = 4::[] in a 22:28:18 error: 22:28:18 • Expecting one more argument to ‘[]’ 22:28:18 Expected a type, but ‘[]’ has kind ‘* -> *’ 22:28:25 apparently not 22:28:35 :t join(.) 22:28:36 > let two :: (forall x. (x -> x) -> (x -> x)) = \ a b -> a (a b) in two (+1) 0 22:28:37 (a -> a) -> a -> a 22:28:38 error: 22:28:38 • Couldn't match expected type ‘forall x1. (x1 -> x1) -> x1 -> x1’ 22:28:38 with actual type ‘(t0 -> t0) -> t0 -> t0’ 22:28:51 > join(.)(join(.))succ 0 22:28:53 4 22:29:25 > let two a b :: ((x -> x) -> (x -> x)) = a (a b) in two (+1) 0 22:29:26 :1:5: error: Parse error in pattern: two 22:29:41 > let (two :: ((x -> x) -> (x -> x))) a b = a (a b) in two (+1) 0 22:29:43 :1:5: error: 22:29:43 Parse error in pattern: (two :: ((x -> x) -> (x -> x))) 22:30:02 hmm 22:30:09 > let two a b = a (a b) in two (+1) 0 22:30:11 2 22:30:18 it works just fine without the type annotation :-P 22:30:41 > let two :: (x -> x) -> x -> x; two = \f x. f (f x) in two two succ 0 22:30:43 :1:42: error: parse error on input ‘.’ 22:30:49 > let two :: (x -> x) -> x -> x; two = \f x -> f (f x) in two two succ 0 22:30:51 4 22:30:56 > let two :: (x -> x) -> x -> x; two = \f x -> f (f x) in two two two succ 0 22:30:58 16 22:31:24 you don't need the annotation 22:31:35 > let two = (\f x -> f (f x)) :: (x -> x) -> x -> x in two two two succ 0 22:31:38 16 22:31:43 subleq: I know. 22:32:01 I wonder whether there was a reason for disabling the pattern type signatures though... I forgot. 22:32:26 > let two :: (x -> x) -> x -> x; two = \f x -> f (f x) in let three :: (x -> x) -> x -> x; three = \f x -> f (f (f x)) in let eight :: (x -> x) -> x -> x; eight = two three in eight (+1) 0 22:32:28 9 22:32:35 bleh, got the arguments backwards 22:32:37 :) 22:32:41 > let two :: (x -> x) -> x -> x; two = \f x -> f (f x) in let three :: (x -> x) -> x -> x; three = \f x -> f (f (f x)) in let eight :: (x -> x) -> x -> x; eight = three two in eight (+1) 0 22:32:43 8 22:32:58 that's what I was checking for, if we could do arithmetic and yet still have the same types 22:33:01 8 == 9 for large values of 8 22:33:01 -!- spieglau has joined. 22:33:15 ais523: you can but only on constants, I think 22:33:30 > let f two = two two in f (\f x -> f (f x)) succ 0 22:33:32 error: 22:33:33 • Occurs check: cannot construct the infinite type: t ~ t -> t1 22:33:33 • In the first argument of ‘two’, namely ‘two’ 22:33:34 I should have gone with 16, 2⁴ = 4² so it wouldn't matter if I had it backwards 22:34:11 -!- ais523 has quit (Remote host closed the connection). 22:34:24 -!- ais523 has joined. 22:34:29 > let f :: (forall x. (x -> x) -> x -> x) -> (x -> x) -> x -> x; f two = two two in f (\f x -> f (f x)) succ 0 22:34:31 4 22:34:54 right, seems like you need the explicit type annotation 22:35:05 which means that the subset of Haskell that uses only ( = ) ; probably isn't TC after all 22:35:37 it's probably TC if you add : 22:35:38 (it works with this higher order type, but that can't be written in the (=); fragment, and it's not Haskell 2010 22:36:22 something I learned while doing literature review for my PhD thesis is that it's been proven that type inference for system F is impossible in general 22:36:32 which is why languages in practice need the annotations 22:37:02 what can system f do that hindley milner can't? 22:37:26 subleq: it has polymorphic arguments 22:37:45 subleq: use the same argument twice (or more) with a different type for each use 22:37:57 oh, like rank-n types 22:38:03 hindley-milner lets you use the same argument multiple times in a lambda but it has to have the same type with each use 22:38:34 > let f :: (forall x. x -> x) -> ((), Bool); f g = (g (), g True) in f id 22:38:36 ((),True) 22:38:51 > let f g = (g (), g True) in f id 22:38:53 error: 22:38:53 • Couldn't match expected type ‘()’ with actual type ‘Bool’ 22:38:53 • In the first argument of ‘g’, namely ‘True’ 22:39:02 this basic idea (with respect to lambda calculi in general, not hindley-milner in particular) is key to the main result of my thesis, which invalidated several years' worth of work in a number of different research projects (including my own) 22:39:08 by showing that what they were aiming for was impossible :_D 22:39:11 * :-D 22:39:23 (that's one of the simplest examples of the difference) 22:46:43 -!- ais523 has quit (Quit: quit). 22:51:04 -!- zzo38 has joined. 23:07:55 I have received the new issue of 2600 today. 23:15:58 vote: 23:16:08 1. going to bed and gettting some healthy sleep 23:16:19 2. ordering a pizza and staying up late 23:16:40 also i'm on a no carb diet so the pizza is like super taboo 23:59:42 -!- lifthrasiir has quit (Quit: No Ping reply in 180 seconds.).