Skip to main content
Added proof in case of fresh renamings.
Source Link
Danny
  • 131
  • 3

Another attempt at explaining why the first definition doesn't work, so assume that we are using that definition.

Let the only sort be $\mathsf{Exp}$, let $\mathcal{X}_{\mathsf{Exp}} = \{y,z\}$, and let $x$ be a variable (of sort $\mathsf{Exp}$) that is fresh for $\mathcal{X}$. Then $y,z \in \mathcal{B}[\mathcal{X}]_{\mathsf{Exp}}$ and $x \in \mathcal{B}[\mathcal{X},x]_{\mathsf{Exp}}$, which implies that

$$ \mathtt{let}(y; x.\!x) \in \mathcal{B}[\mathcal{X}]_{\mathsf{Exp}}, $$

since $\mathtt{let}$ has generalised(generalised) arity $(\mathsf{Exp}, \mathsf{Exp}.\!\mathsf{Exp})\mathsf{Exp}$. In order to show (the false proposition) that

$$ \mathtt{let}(z; x.\!\mathtt{let}(y; x.\!x)) \in \mathcal{B}[\mathcal{X}]_{\mathsf{Exp}}, $$

we would need $\mathtt{let}(y; x.\!x)$ to not only be in $\mathcal{B}[\mathcal{X}]_{\mathsf{Exp}}$, but also in $\mathcal{B}[\mathcal{X,x}]_{\mathsf{Exp}}$. And this is what is impossible, since this requires $x$ to be fresh for $\mathcal{X},x$. (For ABTs with fresh renaming $\mathcal{X} \subseteq \mathcal{Y}$ implies $\mathcal{B}[\mathcal{X}] \subseteq \mathcal{B}[\mathcal{Y}]$, cf. Exercise 1.2, but this doesn't hold for ABTs without fresh renaming.)


Instead use the second definition of ABTs. Let $\rho(x) = x'$ be a fresh renaming of $x$ (relative to $\mathcal{X}$), and let $\rho'(x') = x''$ be a fresh renaming relative to $\mathcal{X},x$. Then $\hat{\rho}'(x') = \rho(x') = x'' \in \mathcal{B}[\mathcal{X},x',x'']_{\mathsf{Exp}}$, so we have

$$ \mathtt{let}(y; x'\!.\!x') \in \mathcal{B}[\mathcal{X},x']_{\mathsf{Exp}}, $$

since $\rho'$ was an arbitrary fresh renaming of $x'$. Next we have

$$ \hat{\rho}(\mathtt{let}(y; x.\!x)) = \mathtt{let}(y; x'\!.\!x') \in \mathcal{B}[\mathcal{X},x']_{\mathsf{Exp}}, $$

and since $\rho$ was an arbitrary fresh renaming of $x$, this implies that

$$ \mathtt{let}(z; x.\!\mathtt{let}(y; x.\!x)) \in \mathcal{B}[\mathcal{X}]_{\mathsf{Exp}}. $$

Another attempt at explaining why the first definition doesn't work.

Let the only sort be $\mathsf{Exp}$, let $\mathcal{X}_{\mathsf{Exp}} = \{y,z\}$, and let $x$ be a variable (of sort $\mathsf{Exp}$) that is fresh for $\mathcal{X}$. Then $y,z \in \mathcal{B}[\mathcal{X}]_{\mathsf{Exp}}$ and $x \in \mathcal{B}[\mathcal{X},x]_{\mathsf{Exp}}$, which implies that

$$ \mathtt{let}(y; x.\!x) \in \mathcal{B}[\mathcal{X}]_{\mathsf{Exp}}, $$

since $\mathtt{let}$ has generalised arity $(\mathsf{Exp}, \mathsf{Exp}.\!\mathsf{Exp})\mathsf{Exp}$. In order to show (the false proposition) that

$$ \mathtt{let}(z; x.\!\mathtt{let}(y; x.\!x)) \in \mathcal{B}[\mathcal{X}]_{\mathsf{Exp}}, $$

we would need $\mathtt{let}(y; x.\!x)$ to not only be in $\mathcal{B}[\mathcal{X}]_{\mathsf{Exp}}$, but also in $\mathcal{B}[\mathcal{X,x}]_{\mathsf{Exp}}$. And this is what is impossible, since this requires $x$ to be fresh for $\mathcal{X},x$. (For ABTs with fresh renaming $\mathcal{X} \subseteq \mathcal{Y}$ implies $\mathcal{B}[\mathcal{X}] \subseteq \mathcal{B}[\mathcal{Y}]$, cf. Exercise 1.2, but this doesn't hold for ABTs without fresh renaming.)

Another attempt at explaining why the first definition doesn't work, so assume that we are using that definition.

Let the only sort be $\mathsf{Exp}$, let $\mathcal{X}_{\mathsf{Exp}} = \{y,z\}$, and let $x$ be a variable (of sort $\mathsf{Exp}$) that is fresh for $\mathcal{X}$. Then $y,z \in \mathcal{B}[\mathcal{X}]_{\mathsf{Exp}}$ and $x \in \mathcal{B}[\mathcal{X},x]_{\mathsf{Exp}}$, which implies that

$$ \mathtt{let}(y; x.\!x) \in \mathcal{B}[\mathcal{X}]_{\mathsf{Exp}}, $$

since $\mathtt{let}$ has (generalised) arity $(\mathsf{Exp}, \mathsf{Exp}.\!\mathsf{Exp})\mathsf{Exp}$. In order to show (the false proposition) that

$$ \mathtt{let}(z; x.\!\mathtt{let}(y; x.\!x)) \in \mathcal{B}[\mathcal{X}]_{\mathsf{Exp}}, $$

we would need $\mathtt{let}(y; x.\!x)$ to not only be in $\mathcal{B}[\mathcal{X}]_{\mathsf{Exp}}$, but also in $\mathcal{B}[\mathcal{X,x}]_{\mathsf{Exp}}$. And this is what is impossible, since this requires $x$ to be fresh for $\mathcal{X},x$. (For ABTs with fresh renaming $\mathcal{X} \subseteq \mathcal{Y}$ implies $\mathcal{B}[\mathcal{X}] \subseteq \mathcal{B}[\mathcal{Y}]$, cf. Exercise 1.2, but this doesn't hold for ABTs without fresh renaming.)


Instead use the second definition of ABTs. Let $\rho(x) = x'$ be a fresh renaming of $x$ (relative to $\mathcal{X}$), and let $\rho'(x') = x''$ be a fresh renaming relative to $\mathcal{X},x$. Then $\hat{\rho}'(x') = \rho(x') = x'' \in \mathcal{B}[\mathcal{X},x',x'']_{\mathsf{Exp}}$, so we have

$$ \mathtt{let}(y; x'\!.\!x') \in \mathcal{B}[\mathcal{X},x']_{\mathsf{Exp}}, $$

since $\rho'$ was an arbitrary fresh renaming of $x'$. Next we have

$$ \hat{\rho}(\mathtt{let}(y; x.\!x)) = \mathtt{let}(y; x'\!.\!x') \in \mathcal{B}[\mathcal{X},x']_{\mathsf{Exp}}, $$

and since $\rho$ was an arbitrary fresh renaming of $x$, this implies that

$$ \mathtt{let}(z; x.\!\mathtt{let}(y; x.\!x)) \in \mathcal{B}[\mathcal{X}]_{\mathsf{Exp}}. $$

Source Link
Danny
  • 131
  • 3

Another attempt at explaining why the first definition doesn't work.

Let the only sort be $\mathsf{Exp}$, let $\mathcal{X}_{\mathsf{Exp}} = \{y,z\}$, and let $x$ be a variable (of sort $\mathsf{Exp}$) that is fresh for $\mathcal{X}$. Then $y,z \in \mathcal{B}[\mathcal{X}]_{\mathsf{Exp}}$ and $x \in \mathcal{B}[\mathcal{X},x]_{\mathsf{Exp}}$, which implies that

$$ \mathtt{let}(y; x.\!x) \in \mathcal{B}[\mathcal{X}]_{\mathsf{Exp}}, $$

since $\mathtt{let}$ has generalised arity $(\mathsf{Exp}, \mathsf{Exp}.\!\mathsf{Exp})\mathsf{Exp}$. In order to show (the false proposition) that

$$ \mathtt{let}(z; x.\!\mathtt{let}(y; x.\!x)) \in \mathcal{B}[\mathcal{X}]_{\mathsf{Exp}}, $$

we would need $\mathtt{let}(y; x.\!x)$ to not only be in $\mathcal{B}[\mathcal{X}]_{\mathsf{Exp}}$, but also in $\mathcal{B}[\mathcal{X,x}]_{\mathsf{Exp}}$. And this is what is impossible, since this requires $x$ to be fresh for $\mathcal{X},x$. (For ABTs with fresh renaming $\mathcal{X} \subseteq \mathcal{Y}$ implies $\mathcal{B}[\mathcal{X}] \subseteq \mathcal{B}[\mathcal{Y}]$, cf. Exercise 1.2, but this doesn't hold for ABTs without fresh renaming.)