k-user AT lists.cs.illinois.edu
Subject: K-user mailing list
List archive
- From: Andrej Tokarčík <andrejtokarcik AT gmail.com>
- To: Derek Sorensen <derek AT pyrofex.net>
- Cc: k-user AT lists.cs.illinois.edu
- Subject: Re: [[K-user] ] Alpha Equivalence
- Date: Tue, 26 Jun 2018 00:59:51 +0200
- Authentication-results: illinois.edu; spf=pass smtp.mailfrom=andrejtokarcik AT gmail.com; dkim=pass header.d=gmail.com header.s=20161025; dmarc=pass header.from=gmail.com
Hey Derek,
You could check out the function `#unifiable` from unification.k.
In particular, this seems to work when attempting to check whether the
loaded $PGM expression is alpha-equivalent to the identity function:
require "unification.k"
module LAMBDA
imports DOMAINS
imports UNIFICATION
syntax Val ::= Id
| "lambda" Id "." Exp [binder]
syntax Exp ::= Val
| Exp Exp [left]
| "(" Exp ")" [bracket]
syntax KVariable ::= Id
syntax Bool ::= isAlphaEquiv(Exp, Exp) [function]
rule isAlphaEquiv(E1, E2) => #unifiable(E1, E2)
configuration <k> isAlphaEquiv($PGM:Exp, lambda ?X . ?X) </k>
endmodule
(Note that I kompiled with `--backend java`, the default OCaml backend
apparently doesn't support unification yet.)
Kind regards,
Andrej
On Mon, Jun 18, 2018 at 10:45 PM, Derek Sorensen
<derek AT pyrofex.net>
wrote:
> Hi all,
>
> Is there a natural/builtin way to do alpha equivalence in K?
>
> Derek
- [[K-user] ] Alpha Equivalence, Derek Sorensen, 06/18/2018
- Re: [[K-user] ] Alpha Equivalence, Andrej Tokarčík, 06/25/2018
Archive powered by MHonArc 2.6.19.