00:16:51 <esowiki> [[Stupid]] M https://esolangs.org/w/index.php?diff=56850&oldid=56558 * Oerjan * (-27) rm nonexistent category
00:17:18 <esowiki> [[Stop]] M https://esolangs.org/w/index.php?diff=56851&oldid=56564 * Oerjan * (-27) rm nonexistent category
00:19:32 <esowiki> [[EsoScript]] M https://esolangs.org/w/index.php?diff=56852&oldid=56822 * Oerjan * (-4) fix category
00:19:50 <esowiki> [[Bit Stupid]] M https://esolangs.org/w/index.php?diff=56853&oldid=56562 * Oerjan * (-27) rm nonexistent category
00:20:29 <esowiki> [[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 <esowiki> [[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 <esowiki> [[Telegram]] https://esolangs.org/w/index.php?diff=56856&oldid=26665 * A * (+578) Unsure...
02:50:04 <esowiki> [[Telegram]] https://esolangs.org/w/index.php?diff=56857&oldid=56856 * A * (+7) Aw man...too messy!
02:53:23 <esowiki> [[User:A]] https://esolangs.org/w/index.php?diff=56858&oldid=56855 * A * (+15)
03:05:04 <esowiki> [[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 <esowiki> [[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 <esowiki> [[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 <esowiki> [[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 <esowiki> [[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 <esowiki> [[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:31:53 <Lean1> 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:52 <HackEso> olist 1128: shachaf oerjan Sgeo FireFly boily nortti b_jonas
19:30:20 -!- nchambers has changed nick to uplime.
19:39:43 <esowiki> [[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 <subleq> Are there any formal languages that do not always halt, but have a decideable halting problem?
21:19:12 <ais523> it's fairly easy to create one
21:19:27 <ais523> but finite state automata with halt states are the most obvious example
21:19:39 <ais523> any infinite loop in those is detectable, so you can just run them until they halt or enter an infinite loop
21:20:17 <ais523> I think even with PDAs, all infinite loops are detectable, but I'm less sure on that
21:28:49 <subleq> you'll see the same state with the same stack iff it doesn't terminate i think
21:29:23 <ais523> not necessarily the same, but the stack will form a repeating pattern
21:29:40 <ais523> so you can see that the loop only looks at, say, the top 10 stack elements before repeating
21:29:54 <ais523> and after that point the top 10 elements are the same, even if they might be at a different position on the stack
21:32:40 <subleq> are there any programming languages equivalent to a PDA?
21:33:35 <esowiki> [[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 <ais523> here: https://esolangs.org/wiki/Category:Push-down_automata
21:33:54 <ais523> Befunge-93 is probably the best known
21:34:56 <esowiki> [[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 <subleq> are you aware of any restrictions on lambda calculus that could work?
21:38:19 <ais523> it's a bit complex, but "all arguments to a recursive or indirectly recursive call must be constants" works
21:38:30 <subleq> i guess just adding a loop primative
21:38:34 <ais523> or https://esolangs.org/wiki/Splinter is pretty similar
21:38:42 <subleq> to a strongly normalizing lambda calculus would work
21:39:14 <ais523> 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 <subleq> i mean something like this https://github.com/edwinb/TypeDD-Samples/blob/master/Chapter11/RunIO.idr
21:50:33 <ais523> actually I'm not certain that any given type in typed lambda calculus has infinitely many functions of that type…
21:52:24 <ais523> like, if there are only finitely many functions of each type
21:52:39 <ais523> 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 <subleq> 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 <ais523> well, you can normally define "provably not halting" as a form of halting all of its own
21:57:30 <ais523> because if you can prove it doesn't halt, now you know the eventual fate of the program
21:57:42 <ais523> from that point of view, decidably-halting and always-halting aren't very different
22:05:45 <esowiki> [[]] 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 <int-e> 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 <subleq> hmm, that paper is not publically available
22:17:26 <ais523> subleq: oh yes, it's obviously TC if you add integers + basic operations on them (like increment, decrement, zero-test)
22:17:55 <subleq> i don't get it, why aren't church numerals equivalent to primitive integers?
22:18:11 <ais523> subleq: the types get increasingly complex as the numbers get larger
22:18:27 <ais523> 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:51 <ais523> 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 <ais523> hmm, I wonder if this invalidates the TCness proof for (=); Haskell
22:21:37 <ais523> or if those characters are enough for TCness some other way
22:23:06 <int-e> > let (===)==(====)=(===) in 0==3
22:24:16 <subleq> so stlc with fix is not turing complete, but seemingly system f with fix is
22:25:42 <int-e> Yeah, System F has proper Church numerals. (of type forall a. (a -> a) -> a -> a)
22:26:35 <ais523> 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 <ais523> > let two : (x -> x) -> (x -> x) = \ a b -> a (a b) in two (+1) 0
22:27:16 <int-e> yeah but it's not System F, just Hindley-Milner... so (as far as I'm concerned) it needs some thought.
22:27:17 <lambdabot> <hint>:1:20: error: parse error on input ‘->’
22:27:28 <ais523> > let two : (x -> x) -> (x -> x) = \ a b => a (a b) in two (+1) 0
22:27:29 <lambdabot> <hint>:1:20: error: parse error on input ‘->’
22:27:40 <ais523> > let two : ((x -> x) -> (x -> x)) = \ a b -> a (a b) in two (+1) 0
22:27:42 <lambdabot> Pattern syntax in expression context: x -> x
22:27:48 <ais523> > let two :: ((x -> x) -> (x -> x)) = \ a b -> a (a b) in two (+1) 0
22:27:50 <lambdabot> • You cannot bind scoped type variable ‘x’
22:28:00 <ais523> I don't actually know Haskell syntax
22:28:08 <ais523> also I thought :: was lists
22:28:18 <lambdabot> • Expecting one more argument to ‘[]’
22:28:18 <lambdabot> Expected a type, but ‘[]’ has kind ‘* -> *’
22:28:36 <ais523> > let two :: (forall x. (x -> x) -> (x -> x)) = \ a b -> a (a b) in two (+1) 0
22:28:38 <lambdabot> • Couldn't match expected type ‘forall x1. (x1 -> x1) -> x1 -> x1’
22:28:38 <lambdabot> with actual type ‘(t0 -> t0) -> t0 -> t0’
22:28:51 <int-e> > join(.)(join(.))succ 0
22:29:25 <ais523> > let two a b :: ((x -> x) -> (x -> x)) = a (a b) in two (+1) 0
22:29:26 <lambdabot> <hint>:1:5: error: Parse error in pattern: two
22:29:41 <ais523> > let (two :: ((x -> x) -> (x -> x))) a b = a (a b) in two (+1) 0
22:29:43 <lambdabot> Parse error in pattern: (two :: ((x -> x) -> (x -> x)))
22:30:09 <ais523> > let two a b = a (a b) in two (+1) 0
22:30:18 <ais523> it works just fine without the type annotation :-P
22:30:41 <int-e> > let two :: (x -> x) -> x -> x; two = \f x. f (f x) in two two succ 0
22:30:43 <lambdabot> <hint>:1:42: error: parse error on input ‘.’
22:30:49 <int-e> > let two :: (x -> x) -> x -> x; two = \f x -> f (f x) in two two succ 0
22:30:56 <int-e> > let two :: (x -> x) -> x -> x; two = \f x -> f (f x) in two two two succ 0
22:31:24 <subleq> you don't need the annotation
22:31:35 <int-e> > let two = (\f x -> f (f x)) :: (x -> x) -> x -> x in two two two succ 0
22:32:01 <int-e> I wonder whether there was a reason for disabling the pattern type signatures though... I forgot.
22:32:26 <ais523> > 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:35 <ais523> bleh, got the arguments backwards
22:32:41 <ais523> > 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:58 <ais523> that's what I was checking for, if we could do arithmetic and yet still have the same types
22:33:01 <int-e> 8 == 9 for large values of 8
22:33:01 -!- spieglau has joined.
22:33:15 <int-e> ais523: you can but only on constants, I think
22:33:30 <int-e> > let f two = two two in f (\f x -> f (f x)) succ 0
22:33:33 <lambdabot> • Occurs check: cannot construct the infinite type: t ~ t -> t1
22:33:33 <lambdabot> • In the first argument of ‘two’, namely ‘two’
22:33:34 <ais523> 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 <int-e> > 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:54 <ais523> right, seems like you need the explicit type annotation
22:35:05 <ais523> which means that the subset of Haskell that uses only ( = ) ; probably isn't TC after all
22:35:37 <ais523> it's probably TC if you add :
22:35:38 <int-e> (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 <ais523> 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 <ais523> which is why languages in practice need the annotations
22:37:02 <subleq> what can system f do that hindley milner can't?
22:37:26 <int-e> subleq: it has polymorphic arguments
22:37:45 <ais523> subleq: use the same argument twice (or more) with a different type for each use
22:38:03 <ais523> 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 <int-e> > let f :: (forall x. x -> x) -> ((), Bool); f g = (g (), g True) in f id
22:38:51 <int-e> > let f g = (g (), g True) in f id
22:38:53 <lambdabot> • Couldn't match expected type ‘()’ with actual type ‘Bool’
22:38:53 <lambdabot> • In the first argument of ‘g’, namely ‘True’
22:39:02 <ais523> 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 <ais523> by showing that what they were aiming for was impossible :_D
22:39:23 <int-e> (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 <zzo38> I have received the new issue of 2600 today.
23:16:08 <izabera> 1. going to bed and gettting some healthy sleep
23:16:19 <izabera> 2. ordering a pizza and staying up late
23:16:40 <izabera> 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.).