2025/06/06

Newest at the top

2025-06-06 22:07:57 +0200trickard_(~trickard@cpe-53-98-47-163.wireline.com.au)
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 +0200sabathan2(~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
2025-06-06 22:06:29 +0200prdak1prdak
2025-06-06 22:06:29 +0200prdak(~Thunderbi@user/prdak) (Ping timeout: 265 seconds)
2025-06-06 22:06:23 +0200trickard_(~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 +0200sabathan2(~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 +0200prdak1(~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 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-06-06 22:01:23 +0200sabathan2(~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 +0200sabathan2(~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 +0200trickard_(~trickard@cpe-53-98-47-163.wireline.com.au)
2025-06-06 21:57:26 +0200tromp(~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 +0200bitdex(~bitdex@gateway/tor-sasl/bitdex) bitdex
2025-06-06 21:55:04 +0200bitdex(~bitdex@gateway/tor-sasl/bitdex) (Remote host closed the connection)
2025-06-06 21:54:53 +0200sabathan2(~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
2025-06-06 21:54:29 +0200sabathan2(~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
2025-06-06 21:51:43 +0200loreto(~loreto@user/loreto) loreto
2025-06-06 21:51:31 +0200loreto(~loreto@user/loreto) (Remote host closed the connection)
2025-06-06 21:51:18 +0200euphores(~SASL_euph@user/euphores) euphores
2025-06-06 21:50:35 +0200ljdarj1(~Thunderbi@user/ljdarj) (Ping timeout: 244 seconds)
2025-06-06 21:50:35 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds)
2025-06-06 21:48:25 +0200sabathan2(~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
2025-06-06 21:48:07 +0200ljdarj(~Thunderbi@user/ljdarj) (Ping timeout: 265 seconds)
2025-06-06 21:48:03 +0200sabathan2(~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Remote host closed the connection)
2025-06-06 21:46:28 +0200ljdarj1(~Thunderbi@user/ljdarj) ljdarj
2025-06-06 21:45:47 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-06-06 21:44:40 +0200trickard_(~trickard@cpe-53-98-47-163.wireline.com.au) (Ping timeout: 252 seconds)
2025-06-06 21:43:52 +0200euphores(~SASL_euph@user/euphores) (Ping timeout: 244 seconds)