From 7d7ed443af66ead7fc50d050069f17a37977e9a9 Mon Sep 17 00:00:00 2001 From: acondolu Date: Thu, 7 Jun 2018 09:28:03 +0200 Subject: [PATCH] Syntactic fixes to distinction + Some commented out definitions to be used in the future --- notes.tex | 97 ++++++++++++++++++++++++++++++++++++++++++++++++++++--- 1 file changed, 92 insertions(+), 5 deletions(-) diff --git a/notes.tex b/notes.tex index 15a8851..1f3f2e5 100644 --- a/notes.tex +++ b/notes.tex @@ -59,14 +59,101 @@ % \item \textbf{Our subproblem:} Semi-$\sigma$-separating two (usual) $\boldsymbol\lambda$-terms % (in deep normal form) \item \textbf{Subterm:} $\SubtmOf\tm\tmtwo$ means that $\tm$ is an ($\eta/\Omega$)-subterm of $\tmtwo$. - \item \textbf{Distinction:} Let $T_x \defeq \{t \preceq T \mid \HeadOf{t} = \HeadOf{D} \}$. - Now: $C_x$ is $D$--\emph{distinct} iff it is empty, or there exists path $\pi$ s.t.: + \item \textbf{Distinction:} Let $\var\defeq \HeadOf D$. Let $T_{\var} \defeq \{\tm \preceq T \mid \HeadOf{\tm} = \var \}$. + $C_{\var}$ is $D$--\emph{distinct} iff it is empty, or there exists path $\pi$ s.t.: \begin{itemize} \item \emph{effective} for $D$, cioe' $\FstOf{\pi} \leq \DegOf{D}$; - \item $\forall t\in D_x$, $t_\pi \neq \Omega$; - \item $\exists t\in C_x$ s.t. $t \not\sim_\pi D$; - \item $\{t\in C_x \mid t \sim_\pi D\}$ is $D$--distinct. + \item $\forall \tm\in D_\var$, $\tm_\pi \neq \Omega$; + \item $\exists \tm\in C_\var$ s.t. $\tm \not\sim_\pi D$; + \item $\{\tm\in C_\var \mid \tm \sim_\pi D\}$ is $D$--distinct. \end{itemize} + + % \item \textbf{Unlockable variables.} + % We use the following contexts: + % $E ::= \Box \mid E\, t \mid t\, E \mid \Lam\var{\vec t\Comma E \Comma \vec t} $. + % A variable $\var$ is \emph{unlockable} in a context $E$ if: + % \begin{itemize} + % \item it is not bound in $E$, or + % \item $E[\cdot] = E'[\vartwo\, \vec\tm \, (\Lam{\cdots\var\cdots}{\vec\tmtwo \Comma E'[\cdot]\Comma\vec\tmthree})]$ + % and $\vartwo$ is unlockable in $E'$. + % \end{itemize} + \end{itemize} +% \clearpage +% \section*{NP-hardness} +% \newcommand{\Pacman}{\Omega} +% \newcommand{\sep}{\cdot} +% \begin{example}[Graph 3-coloring]\label{example:3col} +% Let $G=(V,E)$ be a graph, with $N \defeq |V|$. +% We encode the problem of finding a 3-coloring of $G$ in the following problem of semi-$\sigma$-separation: +% \[\begin{array}{cl} +% \Uparrow & x \sep t_1^1\,t_1^2\,t_1^3 \sep t_2^1\,t_2^2\,t_2^3 \sep \cdots t_n^1\,t_n^2\,t_n^3 \\ +% \\ +% \Downarrow & x \sep \Pacman\,\Pacman\,\Pacman \sep t_2^1\,t_2^2\,t_2^3 \sep \cdots t_n^1\,t_n^2\,t_n^3 \\ +% \Downarrow & x \sep t_1^1\,t_1^2\,t_1^3 \sep \Pacman\,\Pacman\,\Pacman \sep \cdots t_n^1\,t_n^2\,t_n^3 \\ +% \vdots & \vdots \\ +% \Downarrow & x \sep t_1^1\,t_1^2\,t_1^3 \sep t_2^1\,t_2^2\,t_2^3 \sep \cdots \Pacman\,\Pacman\,\Pacman \\ +% \end{array}\] +% +% Where: $\dummy$ is (probably) a variable, $\bomb\defeq \lambda\_.\,\bot$, and the $a$'s are defined as follows: +% +% \begin{itemize} +% +% \item $\begin{array}{ll} +% a_1^1 \defeq & \lambda\_. \, x \sep y\bomb\bomb \sep\bomb\ldots \\ +% a_1^2 \defeq & \lambda\_. \, x \sep \bomb y\bomb \sep\bomb\ldots \\ +% a_1^3 \defeq & \lambda\_. \, x \sep \bomb\bomb y \sep\bomb\ldots \\ +% \end{array}$ +% +% \item $a_2^1 \defeq \begin{cases} +% \lambda\_.\, x \sep \bomb \dummy\dummy \sep y\bomb\bomb \cdot \bomb\ldots & \text{if } (v_1, v_2)\in E \\ +% \lambda\_.\, x \sep \dummy\dummy\dummy \sep y\bomb\bomb \cdot \bomb\ldots & \text{if } (v_1, v_2)\not\in E \\ +% \end{cases}$ +% +% \item \ldots +% +% \end{itemize} +% +% \begin{definition}[Index notation] +% Let $t = x \sep x_1^1 x_2^1 x_3^1 \sep x_1^2 x_2^2 x_3^2 \sep \ldots \sep x_1^m x_2^m x_3^m$. Then: \[t[\,_k^j] \defeq x_k^j.\] +% \end{definition} +% +% Let $z_0$, $z_1$, $z_2$ be variables. +% +% Define: +% \[a_k^j[\,_{k'}^{j'}]\defeq\begin{cases} +% \bomb & \text{if } j