Skip to Content.
Sympa Menu

k-user - Re: [[K-user] ] Alpha Equivalence

k-user AT lists.cs.illinois.edu

Subject: K-user mailing list

List archive

Re: [[K-user] ] Alpha Equivalence


Chronological Thread 
  • 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



Archive powered by MHonArc 2.6.19.

Top of Page