Alpha-equivalence

Then, =_\\alpha ParseError: Got function '\\' with no arguments as subscript at position 3: =_\̲\̲alpha is the strongest Congruence on $\begin{array}{l}\\ mathcalA\end{array}$that contains the followings:

• Formal definition according to Practical foundations for programming languages

  Consider:

  • A fixed set of Sort $𝒮$, which categorize ASTs into Syntactic category.

  • A sort-indexed family of Variables $𝒳=\{{𝒳}_s\}$, where ${𝒳}_s$ is the set of variables with sort $𝒮$. A sequence of variable is written as $\overrightarrow{x}$.

  • A sort-indexed family of Abstract syntax tree (AST)s $𝒜=\{{𝒜}_s\}$, where ${𝒜}_s$ is the set of ASTs with sort $𝒮$.

  • An Arity-indexed family of Operator $𝒪=\{{𝒪}_{\alpha }\}$, where ${𝒪}_{\alpha }$ is the set of operators with the given arity $\alpha$.

  • A fresh renaming with respect to $𝒳$ is a bijection $\rho :\overrightarrow{x}\leftrightarrow \overrightarrow{y}$ such that $\overrightarrow{y}$ is fresh in $𝒳$.

    Then, ${=}_{\alpha }$ is the strongest Congruence on $𝒜$that contains the followings:

  • For $x\in 𝒳$, then $x{=}_{\alpha }x$.

  • For $o\in 𝒪$, then $o({\overrightarrow{x}}_1.a_1;\dots ;{\overrightarrow{x}}_n.a_n){=}_{\alpha }o({\overrightarrow{x}}_1^{\prime }.a_1^{\prime };\dots ;{\overrightarrow{x}}_n^{\prime }.a_n^{\prime })$ if for every $1\le i\le n$, ${\hat{\rho }}_i(a_i){=}_{\alpha }{\hat{\rho }}_i^{\prime }(a_i^{\prime })$ for all fresh renamings ${\rho }_i:{\overrightarrow{x}}_i\leftrightarrow {\overrightarrow{z}}_i$ and ${\rho }_i^{\prime }:{\overrightarrow{x}}_i^{\prime }\leftrightarrow {\overrightarrow{z}}_i$.