K-user mailing list

[Andrej Tokarčík <andrejtokarcik AT 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