From 99d28a7580c2acc8351d550d2b340be0b7445353 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Hans-J=C3=B6rg=20Schurr?= <hansjoerg-schurr@uiowa.edu> Date: Fri, 27 Jan 2023 12:30:04 -0600 Subject: [PATCH] Add language about capture-avoiding --- spec/doc.tex | 32 +++++++++++++++++++++----------- spec/rule_list.tex | 4 ++-- 2 files changed, 23 insertions(+), 13 deletions(-) diff --git a/spec/doc.tex b/spec/doc.tex index 555227f..9232915 100644 --- a/spec/doc.tex +++ b/spec/doc.tex @@ -364,23 +364,30 @@ in bold (e.g., $\lsymb{Bool}$, $\lsymb{ite}$). We will use $θ$ to denote a substitution\index{substitution}. The notation $[x₠↦ tâ‚, …, x_n ↦ t_n]$ denotes the substitution that maps $x_i$ to $t_i$ for $1 ≤ i ≤ n$ and corresponds to the -identity function for all other variables. If $θ$ and $η$ are two +identity function for all other variables. +% +If $θ$ and $η$ are two substitutions, then $θη$ denotes the result of first applying $θ$ and then $η$ (i.e., $η(θ(.))$). A substitution can naturally be extended to a function that maps terms to terms by replacing the occurrences of free variables. % +The application of a substitution $θ$ to a term $t$ (i.e., $θ(t)$) +is capture-avoiding; bound variables in $t$ are renamed as necessary. + We write $t[u]$ for a term that contains the term $u$ as a subterm. If $u$ is subsequently replaced by a term $v$, we write $t[v]$ for the new term. % -We also use this notation with multiple variables. +We also use this notation with multiple terms. % -The notation $t[x_1, \dots, x_n]$ stands for a term may contain the distinct -variables $x_1, \dots, x_n$. +The notation $t[u_1, \dots, u_n]$ stands for a term may contain the +pairwise distinct terms $u_1, \dots, u_n$. % -Then, $t[s_1,\dots, s_n]$ is the respective term where the variables $x_1,\dots, x_n$ are -simultaneously substituted by $s_1,\dots, s_n$. +Then, $t[s_1,\dots, s_n]$ is the respective term where the +variables $u_1,\dots, u_n$ are +simultaneously replaced by $s_1,\dots, s_n$. Usually, $u_1, \dots, u_n$ will +be variables. Note that we will introduce the Alethe specific notation to write proof steps in the following sections. @@ -545,8 +552,7 @@ variable. The second case is a mapping. Throughout this chapter, $\Gamma$ denotes an arbitrary context. -% TODO: define \subst and related -Every context $\Gamma$ induces a substitution +Every context $\Gamma$ induces a capture-avoiding substitution $\subst(\Gamma)$. If $\Gamma$ is the empty list, $\subst(\Gamma)$ is the empty substitution, i.e, the identity function. @@ -564,8 +570,7 @@ with this mapping: \subst([c_1,\dots, c_{n-1}])\circ \{x_n\mapsto t_n\}. \] - -\label{ex:alethe:substctx}The following example illustrates this idea: +\label{ex:alethe:substctx}The following example illustrates this idea. \begin{align*} \subst([x\mapsto 7, x \mapsto g(x)]) &= \{x\mapsto g(7)\} \\ \subst([x\mapsto 7, x, x \mapsto g(x)]) &= \{x\mapsto g(x)\} \\ @@ -581,10 +586,15 @@ where the term $t$\, is the original term, and $u$ is the term after preprocessing. Tautologies with contexts correspond to judgments $\vDash_T \subst(\Gamma)(t) ≈ u$. +Since the substitution induced by a context is capture-avoiding, +applying it might rename bound variables to avoid binding variables +in substituent terms. +This is an implicit term transformation without a proof. Therefore, +the Alethe rules are designed to avoid such contexts. + Formally, the context can be translated to \index{abstraction!lambda}λ-abstractions and applications. This is discussed in Section~\ref{sec:alethe:semantics}. - \begin{example}\label{ex:ti:ctx-abstract} This example shows a proof that uses a subproof with a context to rename a bound variable. diff --git a/spec/rule_list.tex b/spec/rule_list.tex index 479bd14..59891a0 100644 --- a/spec/rule_list.tex +++ b/spec/rule_list.tex @@ -544,8 +544,8 @@ $k$. & & \ctxsep & $\forall x_1, \dots, x_n.\varphi ≈ \forall y_1, \dots, y_n. \varphi'$ & \currule{} \\ \end{AletheXS} - where the variables $y_1, \dots, y_n$ are not free in $\forall x_1, - \dots, x_n.\varphi$. + where the variables $y_1, \dots, y_n$ are neither free in $\forall x_1, + \dots, x_n.\varphi$ nor occur in $\Gamma$. \end{RuleDescription} \begin{RuleDescription}{sko_ex} -- GitLab