Programming Language Theory Flashcard

What is the formal definition for alpha-equivalence?

Books

Concepts

Decklanguage theory

Question

What is the formal definition for alpha-equivalence?

Answer

Alpha-equivalence is a relation $=_{α}$ on the set of terms/ASTs. Given $𝒜$ as a set of ASTs. Then:

$x =_{α} x$ .
$o ({\vec{x}}_{1} . a_{1}; \dots; {\vec{x}}_{n} . a_{n}) =_{α} o ({\vec{x}}_{1}^{'} . a_{1}^{'}; \dots; {\vec{x}}_{n}^{'} . a_{n}^{'})$ if for every $1 \leq i \leq n$ , $ρ_{i} : {\vec{x}}_{i} \leftrightarrow {\vec{z}}_{i}$ and $ρ_{i}^{'} : {\vec{x}}_{i}^{'} \leftrightarrow {\vec{z}}_{i}$ and $ρ_{i} (a_{i}) =_{α} ρ_{i}^{'} (a_{i}^{'})$ .