# Are isomorphic (untyped) lambda expressions semantically equivalent?

"Isomorphic" is defined as having the same shape of syntax trees and the same bindings of variables. However, the variable names might be completely different. In other words, it is to say that we have a graph isomorphism between the two expressions (the graph being the syntax tree with variable linking included as edges). The intuition behind this is that assuming we are given the isomorphism, it is always possible to rename the variables and obtain the other expression.

• You're basically describing $\alpha$ equivalence, though it's not usually phrased as a graph property. – jmite May 11 at 13:26