←2023-11-25 2023-11-26 2023-11-27→ ↑2023 ↑all
00:22:28 -!- Thelie has quit (Remote host closed the connection).
00:25:57 <esolangs> [[Special:Log/newusers]] create * Asdkjadka * New user account
01:17:25 -!- __monty__ has quit (Quit: leaving).
06:04:26 <esolangs> [[Special:Log/newusers]] create * Redisnotblue * New user account
06:06:59 <esolangs> [[Esolang:Introduce yourself]] M https://esolangs.org/w/index.php?diff=119868&oldid=119780 * Redisnotblue * (+189)
06:33:52 -!- tromp has joined.
06:34:31 -!- tromp has quit (Client Quit).
07:04:47 -!- tromp has joined.
07:15:42 -!- tromp has quit (Quit: My iMac has gone to sleep. ZZZzzz…).
07:39:07 -!- tromp has joined.
08:51:50 -!- cpressey has joined.
08:59:53 <cpressey> riv: re forwards and backwards proof: I think of it like this:
08:59:54 <cpressey> A proof is a tree (or more often it's actually a DAG). "Forward proof" is to start at the leaves and work towards the root. "Backward proof" is to start at the root and work towards the leaves.
08:59:54 <cpressey> I think this can sometimes manifest in the way you described with assumptions and conclusions, but not necessarily.
09:08:25 <esolangs> [[Talk:Binary lambda calculus]] https://esolangs.org/w/index.php?diff=119869&oldid=24477 * Squidmanescape * (+2815)
09:16:29 <riv> oh i see!
09:25:02 -!- tromp has quit (Quit: My iMac has gone to sleep. ZZZzzz…).
09:32:55 <esolangs> [[Special:Log/newusers]] create * YOU.. * New user account
09:33:51 -!- Guest36 has joined.
10:06:23 -!- Guest36 has quit (Quit: Client closed).
10:09:31 -!- Lord_of_Life_ has joined.
10:09:41 -!- Lord_of_Life has quit (Ping timeout: 240 seconds).
10:10:56 -!- Lord_of_Life_ has changed nick to Lord_of_Life.
10:26:35 -!- tromp has joined.
10:35:04 <cpressey> This is what I've been working on lately: https://codeberg.org/catseye/define-opaque/src/branch/develop-0.2
10:35:04 <cpressey> My thought is, if you can do it in Scheme, you could do it in the untyped lambda calculus too.
10:35:05 <cpressey> Which would give you a basis to argue that the untyped lambda calculus is strongly typed.
11:27:46 -!- tromp has quit (Quit: My iMac has gone to sleep. ZZZzzz…).
11:29:37 -!- tromp has joined.
11:42:41 -!- Sgeo has quit (Read error: Connection reset by peer).
12:35:28 <b_jonas> cpressey: doesn't a later scheme standard already give you something like that?
12:37:18 <b_jonas> cpressey: I think you're relying on the equal? primitive, that wouldn't work in untyped lambda calculus
12:37:53 <b_jonas> I don't have a proof, but I think it's not possible in untyped lambda calculus
12:43:00 <b_jonas> in untyped lambda calculus, if you can construct a private accessor function then an adversary can also construct the same function
12:43:08 <b_jonas> there's no eq? or other way to distinguish
12:45:40 <b_jonas> that's not quite a proof because it doesn't exclude inside-out structures, but I think you can't hide data that way either in untyped lambda calculus
13:19:21 -!- tromp has quit (Quit: My iMac has gone to sleep. ZZZzzz…).
13:20:49 -!- tromp has joined.
13:27:34 -!- FreeFull has quit.
14:06:49 -!- tromp has quit (Quit: My iMac has gone to sleep. ZZZzzz…).
14:09:41 -!- tromp has joined.
14:47:08 -!- Thelie has joined.
15:05:09 -!- ais523 has joined.
15:10:32 -!- kspalaiologos has joined.
15:44:29 -!- FreeFull has joined.
15:58:33 -!- simcop2387 has quit (Read error: Connection reset by peer).
15:58:33 -!- perlbot has quit (Read error: Connection reset by peer).
16:04:10 -!- perlbot has joined.
16:04:37 -!- simcop2387 has joined.
16:08:15 -!- perlbot has quit (Read error: Connection reset by peer).
16:08:20 -!- simcop2387 has quit (Read error: Connection reset by peer).
16:12:36 -!- perlbot has joined.
16:14:30 -!- perlbot has quit (Read error: Connection reset by peer).
16:19:49 -!- perlbot has joined.
16:23:44 -!- perlbot has quit (Read error: Connection reset by peer).
16:24:16 -!- ais523 has quit (Remote host closed the connection).
16:25:30 -!- ais523 has joined.
16:26:41 -!- perlbot has joined.
16:30:20 -!- simcop2387 has joined.
16:31:08 -!- example99 has joined.
16:31:13 -!- example99 has left.
16:49:29 -!- ais523 has quit (Remote host closed the connection).
16:50:44 -!- ais523 has joined.
17:10:43 <esolangs> [[Lazy evaluation]] https://esolangs.org/w/index.php?diff=119870&oldid=119837 * Quito0567 * (+9)
17:25:25 -!- tromp has quit (Quit: My iMac has gone to sleep. ZZZzzz…).
17:40:20 -!- Koen has joined.
18:31:36 -!- tromp has joined.
18:41:57 -!- Sgeo has joined.
19:03:25 <esolangs> [[Jumping to -1 is exciting]] M https://esolangs.org/w/index.php?diff=119871&oldid=30201 * PythonshellDebugwindow * (+73) Categories
19:04:52 <esolangs> [[Black and white and read all over]] M https://esolangs.org/w/index.php?diff=119872&oldid=18201 * PythonshellDebugwindow * (+9) Stub
19:37:12 -!- simcop2387 has quit (Read error: Connection reset by peer).
19:37:13 -!- perlbot has quit (Read error: Connection reset by peer).
19:39:58 -!- perlbot has joined.
19:58:41 -!- simcop2387 has joined.
21:43:56 <esolangs> [[Lazy evaluation]] https://esolangs.org/w/index.php?diff=119873&oldid=119870 * Quito0567 * (+18)
21:48:17 -!- tromp has quit (Quit: My iMac has gone to sleep. ZZZzzz…).
21:53:03 -!- tromp has joined.
21:53:54 -!- cpressey has quit (Ping timeout: 250 seconds).
22:30:43 -!- Thelie has quit (Remote host closed the connection).
22:33:32 -!- tromp has quit (Quit: My iMac has gone to sleep. ZZZzzz…).
22:40:42 -!- tromp has joined.
22:42:12 -!- Koen has quit (Quit: Leaving...).
22:54:20 -!- tromp has quit (Quit: My iMac has gone to sleep. ZZZzzz…).
23:15:18 -!- tromp has joined.
23:22:36 -!- Sgeo has quit (Read error: Connection reset by peer).
23:22:56 -!- GregorR1 has joined.
23:24:41 -!- GregorR has quit (Ping timeout: 268 seconds).
23:24:41 -!- GregorR1 has changed nick to GregorR.
23:41:54 -!- tromp has quit (Quit: My iMac has gone to sleep. ZZZzzz…).
←2023-11-25 2023-11-26 2023-11-27→ ↑2023 ↑all