Newest at the top
2025-06-06 22:07:13 +0200 | <tomsmeding> | (assuming it changes the body somehow, potentially moving occurrences of the bound variable around) |
2025-06-06 22:07:00 +0200 | <tomsmeding> | the recursive traversal of that body must then take an argument term which it is to put in the new locations of the bound variable |
2025-06-06 22:06:39 +0200 | sabathan2 | (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) |
2025-06-06 22:06:29 +0200 | prdak1 | prdak |
2025-06-06 22:06:29 +0200 | prdak | (~Thunderbi@user/prdak) (Ping timeout: 265 seconds) |
2025-06-06 22:06:23 +0200 | trickard_ | (~trickard@cpe-53-98-47-163.wireline.com.au) (Read error: Connection reset by peer) |
2025-06-06 22:06:20 +0200 | <tomsmeding> | iirc what you do is when you want to inspect the term below a binder, you generate a name for the bound variable |
2025-06-06 22:06:18 +0200 | sabathan2 | (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection) |
2025-06-06 22:05:12 +0200 | <EvanR> | that would answer the original question |
2025-06-06 22:04:57 +0200 | <EvanR> | convert it to a normal datastructure making up names? |
2025-06-06 22:04:41 +0200 | <tomsmeding> | that's the same question as "how do you do _anything_ with a HOAS term" |
2025-06-06 22:04:30 +0200 | <EvanR> | and how do you do that |
2025-06-06 22:04:19 +0200 | <tomsmeding> | where with HOAS, that simplifies to beta-eta equivalence checking |
2025-06-06 22:04:11 +0200 | <tomsmeding> | equivalence checking, as in alpha-beta-eta equivalence checking |
2025-06-06 22:04:08 +0200 | <EvanR> | is where I got lost |
2025-06-06 22:03:55 +0200 | <EvanR> | >Second, programs that are alpha-equivalent (differing only in the names of bound variables) have identical representations in HOAS, which can make equivalence checking more efficient. |
2025-06-06 22:03:25 +0200 | <tomsmeding> | you couldn't check it, but there is nothing to check in the first place |
2025-06-06 22:03:16 +0200 | <tomsmeding> | no, as in, alpha-equivalent terms are always equal functions |
2025-06-06 22:03:04 +0200 | prdak1 | (~Thunderbi@user/prdak) prdak |
2025-06-06 22:02:51 +0200 | <EvanR> | trivial, so just compare functions for equality? xD |
2025-06-06 22:02:48 +0200 | <tomsmeding> | that much is true |
2025-06-06 22:02:43 +0200 | <tomsmeding> | same as with De Bruijn |
2025-06-06 22:02:35 +0200 | <tomsmeding> | alpha-equivalence is trivial with a HOAS representation because there are no names |
2025-06-06 22:02:15 +0200 | <EvanR> | both representations leave you without variable names, but I'm not sure how HAOS makes alpha equivalence easy |
2025-06-06 22:01:34 +0200 | <tomsmeding> | that paragraph does read decidedly oddly |
2025-06-06 22:01:34 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
2025-06-06 22:01:23 +0200 | sabathan2 | (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) |
2025-06-06 22:01:03 +0200 | <EvanR> | wikipedia quality |
2025-06-06 22:01:02 +0200 | sabathan2 | (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Read error: Connection reset by peer) |
2025-06-06 22:00:35 +0200 | <EvanR> | it's conflating HAOS where you implement the function syntax using host language functions with implement the function object using debruijn indices to get the same result |
2025-06-06 21:57:35 +0200 | trickard_ | (~trickard@cpe-53-98-47-163.wireline.com.au) |
2025-06-06 21:57:26 +0200 | tromp | (~textual@2001:1c00:3487:1b00:8836:3ddb:338e:2a33) |
2025-06-06 21:55:37 +0200 | <mjacob> | I’m trying to understand https://en.wikipedia.org/wiki/Higher-order_abstract_syntax#Implementation. In that section, it is said that “another popular way to implement HOAS (in, for example, compilers) is with de Bruijn indices”. Aren’t HOAS and de Bruijn indices different solutions to a similar problem (encoding binding)? |
2025-06-06 21:55:30 +0200 | bitdex | (~bitdex@gateway/tor-sasl/bitdex) bitdex |
2025-06-06 21:55:04 +0200 | bitdex | (~bitdex@gateway/tor-sasl/bitdex) (Remote host closed the connection) |
2025-06-06 21:54:53 +0200 | sabathan2 | (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) |
2025-06-06 21:54:29 +0200 | sabathan2 | (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection) |
2025-06-06 21:51:43 +0200 | loreto | (~loreto@user/loreto) loreto |
2025-06-06 21:51:31 +0200 | loreto | (~loreto@user/loreto) (Remote host closed the connection) |
2025-06-06 21:51:18 +0200 | euphores | (~SASL_euph@user/euphores) euphores |
2025-06-06 21:50:35 +0200 | ljdarj1 | (~Thunderbi@user/ljdarj) (Ping timeout: 244 seconds) |
2025-06-06 21:50:35 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
2025-06-06 21:48:25 +0200 | sabathan2 | (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) |
2025-06-06 21:48:07 +0200 | ljdarj | (~Thunderbi@user/ljdarj) (Ping timeout: 265 seconds) |
2025-06-06 21:48:03 +0200 | sabathan2 | (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection) |
2025-06-06 21:46:28 +0200 | ljdarj1 | (~Thunderbi@user/ljdarj) ljdarj |
2025-06-06 21:45:47 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
2025-06-06 21:44:40 +0200 | trickard_ | (~trickard@cpe-53-98-47-163.wireline.com.au) (Ping timeout: 252 seconds) |
2025-06-06 21:43:52 +0200 | euphores | (~SASL_euph@user/euphores) (Ping timeout: 244 seconds) |
2025-06-06 21:43:15 +0200 | manwithluck | (~manwithlu@2a09:bac5:5082:2432::39b:b0) manwithluck |