questions on formalization of lambda calculus

Stream: general

[Paige Thomas]

I was wondering if anyone might be able to tell me if this is a correct definition of whether a pair of untyped lambda calculus terms are alpha equivalent, and if so, how I can prove that it is.

import Mathlib.Data.Finset.Basic


@[reducible]
def Symbol_ : Type := String
deriving Inhabited, DecidableEq, Repr


inductive Term_ : Type
| var_ : Symbol_ → Term_
| app_ : Term_ → Term_ → Term_
| abs_ : Symbol_ → Term_ → Term_
deriving Inhabited, DecidableEq, Repr


open Term_


/--
  rename u v e := The simultaneous replacement of each occurrence of the variable `u` by the variable `v` in the term `e`.
  (`u -> v` in `e`)
-/
def rename
  (u v : Symbol_) :
  Term_ → Term_
  | var_ x =>
    if u = x
    then var_ v
    else var_ x
  | app_ M N =>
    app_ (rename u v M) (rename u v N)
  | abs_ x M =>
    if u = x
    then abs_ v (rename u v M)
    else abs_ x (rename u v M)


def Term_.var_set :
  Term_ → Finset Symbol_
  | var_ x => {x}
  | app_ M N => M.var_set ∪ N.var_set
  | abs_ x M => M.var_set ∪ {x}


inductive are_alpha_equiv : Term_ → Term_ → Prop

| refl
  (M : Term_) :
  are_alpha_equiv M M

| symm
  (M N : Term_) :
  are_alpha_equiv M N →
  are_alpha_equiv N M

| trans
  (M N P : Term_) :
  are_alpha_equiv M N →
  are_alpha_equiv N P →
  are_alpha_equiv M P

| app
  (M M' N N' : Term_) :
  are_alpha_equiv M M' →
  are_alpha_equiv N N' →
  are_alpha_equiv (app_ M N) (app_ M' N')

| abs
  (x : Symbol_)
  (M M' : Term_) :
  are_alpha_equiv M M' →
  are_alpha_equiv (abs_ x M) (abs_ x M')

| alpha
  (x y : Symbol_)
  (M : Term_) :
  y ∉ M.var_set →
  are_alpha_equiv (abs_ x M) (abs_ y (rename x y M))

[Andrés Goens]

By that definition, var_ "x" and var "y" , with free variables, are not alpha equivalent. So you can't prove alpha equivalence of terms with free variables, not sure if that's what you want...

That being said, how can you ever prove something's the correct definition? You can postulate a bunch of properties you expect your definition to have and prove them, like alpha equivalence actually being an equivalence relation (reflexive, symmetric, and transitive), or depending on your order of evaluation here (you haven't really defined the semantics with substitution and beta), you could prove that you'll get the same result modulo alpha, but all that doesn't prove it's the right definition, does it?

[Paige Thomas]

Hmm. I thought var_ "x" and var "y" should not be alpha equivalent.

[Paige Thomas]

Yes, I'm looking for some defining characteristic of alpha equivalence that holds that I can prove.

[Paige Thomas]

Or a reference to another formalization that defines the same thing, also using named variables.

[Paige Thomas]

Most of what I find use either de Bruijn or locally nameless.

[Paige Thomas]

I was going by this paper: https://www.mscs.dal.ca/~selinger/papers/lambdanotes-2up.pdf

[Paige Thomas]

Kayla Thomas said:

Hmm. I thought var_ "x" and var "y" should not be alpha equivalent.

That is, I don't think I can use my definition to prove that var_ "x" and var "y" are alpha equivalent, and I thought it was correct that they are not alpha equivalent?

[Shreyas Srinivas]

One answer is to convert the terms to a canonical form

[Shreyas Srinivas]

But then the theorem's claim is that two terms are alpha-equivalent under that conversion function upto the correctness of your definition of the canonical form

[Shreyas Srinivas]

In your rename function, it looks like you are renaming bound variables under the binder. This can lead to variable capture

[Paige Thomas]

Shreyas Srinivas said:

In your rename function, it looks like you are renaming bound variables under the binder. This can lead to variable capture

This rename function is not meant to be capture avoiding. I think that should be taken care of by the y ∉ M.var_set condition in the alpha case of are_alpha_equiv.

[Paige Thomas]

I actually have a similar question about the formalization of a capture avoiding substitution definition, but I don't have access to it at the moment.

[Shreyas Srinivas]

Tapl has a chapter on this

[Shreyas Srinivas]

Lean's manual also has some examples of de bruijn indices

[Paige Thomas]

I was hoping to use named variables, but I guess I could prove their equivalence to the named variable definitions.

[Andrés Goens]

Kayla Thomas said:

Kayla Thomas said:

Hmm. I thought var_ "x" and var "y" should not be alpha equivalent.

That is, I don't think I can use my definition to prove that var_ "x" and var "y" are alpha equivalent, and I thought it was correct that they are not alpha equivalent?

right, I looked it up, I always assumed alpha renaming meant just renaming, but it seems to be explicitly only for bound variables (so you're right about this)

[Andrés Goens]

I guess I would argue that the property you'd want is that it's a congruence relation for beta reductions?

[Andrés Goens]

which essentially means that alpha conversion doesn't change the semantics

[Shreyas Srinivas]

That's more complicated than just establishing an alpha equivalence