\documentclass[12pt]{article}
\usepackage{blindtext}
\usepackage{enumerate}
\usepackage{hyperref, bookmark}
\usepackage{amsmath, amsfonts, amssymb, amsthm}
\usepackage{xcolor}

\title{Ideas on Strong Separation}
\author{Anonymous}

\input{macros}
\begin{document}

\maketitle

\renewcommand{\Lam}[2]{\lambda#1.\, \{\!\!\{#2\}\!\!\}}

\subparagraph{Syntax}
\[\begin{array}{lll}
  \tm, \tmtwo & \ddef & \var \mid \tm\,\tmtwo \mid \Lam\var{\tm\Comma\vec\tm} \\
  n & \ddef & \Lam\var{n\Comma\vec n} \mid \var\,\vec n \\
  \\
  C & \ddef & \Box \mid C\,\tm \mid \tm\,C \\
  P & \ddef & \vec\tm \Comma \Box \Comma \vec\tm \mid \vec\tm \Comma C[\Lam\var P] \Comma \vec\tm  \\
\end{array}\]

\subparagraph{Reduction}
\[\begin{array}{lll}
  P[C[(\Lam\var{\tm\Comma\vec\tm})\,\tmtwo]] & \Red{}{\var\in \tm,\vec\tm} &
   P[C[\tm\Subst\var\tmtwo]\Comma \vec\tm\Subst\var\tmtwo]\\
   P[C[(\Lam\var{\tm\Comma\vec\tm})\,\tmtwo]] & \Red{}{\var\not\in\tm,\vec\tm} &
    P[C[\tm] \Comma \vec\tm\Comma\tmtwo]\\
\end{array}\]

\subparagraph{Properties of the calculus:}
\begin{itemize}
  \item Every term is normalizing iff it is strongly normalizing.
  \item Ogni strategia e' perpetua!
\end{itemize}

\clearpage

\[ E ::= \Box \mid E\, t \mid t\, E \mid \Lam\var{\vec t\Comma E \Comma \vec t} \]

\begin{definition}{Path of a hole}
  \[\begin{array}{ll}
    \pi_\Box & \defeq \langle\rangle \\
    \pi_{\Lam{\vec\var}{\vec i \Comma y \, }y\, \vec t E \vec s} & \defeq \\
  \end{array}\]
\end{definition}

\newcommand{\NameOf}[2]{\operatorname{name}_{#2}(#1)}
\begin{definition}[Name of a variable]~
  \begin{itemize}
    \item If $\var$ is free in $\tm$, then $\NameOf\var\tm = ``\var"$;
    \item {\color{red} If $x$ is bound at the outer layer of a garbage, then
     $\NameOf\var\tm = \Omega$;}
    \item
    If $ x\, \vec s \, (\lambda \vec y.\, \ldots) \preceq t$, then
    $ \NameOf{\vartwo_i}{\tm} \defeq \NameOf\var\tm ; (|\vec s|, i) $.
  \end{itemize}
\end{definition}

\begin{example}
  \[\begin{array}{ll}
  D & x \, a \, (\Lam\vartwo {y \Comma y\, b} ) \\
  C & x \, a \, (\Lam\vartwo{y \Comma y \,b'}) \\
  C & x \, a' \, (\Lam\vartwo{y \Comma y \,b }) \\
  \end{array}\]

  \[\begin{array}{ll}
  D & y^{[x \, a \, \Omega]} \, b \\
  C & y^{[x \, a \, \Omega]} \, b' \\
  C & y^{[x \, a' \, \Omega]} \, b \\
  \end{array}\]
\end{example}



\clearpage
\[ E ::= \Box \mid E\, t \mid t\, E \mid \Lam\var{\vec t\Comma E \Comma \vec t} \]

\begin{definition}[Unlockable variable]
  A variable $\var$ is 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{definition}

\begin{lemma}[Elimination of unlockable variables]
  For every set of terms $\tm_1, \ldots, \tm_n$
  there exist terms $\tm'_1, \ldots, \tm'_n$
  without unlockable variables and
  such that $\tm_i$ is unseparable from $\tm'_i$.
\end{lemma}

{\color{red}
 Non esattamente!
 I termini hanno gli stessi path, e le variabili unlockable
 del secondo sono iin path virtuali nel primo

 Piu' esattamente, hai portato il garbage che vuoi far divergere
  al top level.
}

\begin{definition}
  Transformation removing an unlockable variable bound at position $\pi$:
  \[\tau_{n::\pi}[\alpha] := \lambda x_1..x_n\,x.\, \alpha\,\vec x\,(\tau_\pi[x])\]
\end{definition}

{\color{red}
Warning! It creates unlockable variables, but in positions whose paths were
previously virtual}

\begin{lemma}
  For every semi-$\sigma$-separable $\tm$ and $\tmtwo$,
   there exist $\sigma$ s.t $\tm\sigma = \ldots \Comma C[i] \Comma \ldots$
   and $i \not\preceq \tmtwo\sigma$ (and therefore, $\tm\sigma$ and $\tmtwo\sigma$
   are semi-$\sigma$-separable by ???).
\end{lemma}

\begin{theorem}
  $\tm$ and $\tmtwo$ are semi-$\sigma$-separable if \ldots
\end{theorem}

\clearpage
\newcommand{\HeadOf}[1]{\operatorname{hd}(#1)}
\newcommand{\ArityOf}[1]{\operatorname{len}(#1)}
\begin{itemize}
  \item \textbf{A sufficient condition for separability:}
  \item \textbf{Goal.} semi-$\sigma$-separating $\tm$ from $\tmtwo$ (both inerts with pacmans/$\Omega$).
  \item Let $U \defeq \{\tmtwo' \mid \tmtwo'\preceq\tmtwo \land \HeadOf{\tmtwo'}=\HeadOf{\tm}
  \land \ArityOf{\tmtwo'} \leq \ArityOf{\tm}\} = \{u_1, \ldots, u_N\}$.
  \item \textbf{Theorem.} The problem is separable if there exist $\pi_1\ldots\pi_N$
  $\eta$-difference paths between
  $\tm$ and $\tmtwo_1\ldots\tmtwo_N$ that are pairwise compatible on $\tm$ (note: also between themselves).
  \item \textbf{Definition ($\eta$-difference path).}
  \item \textbf{Definition ($\sqsubset$).} Initial fragments of paths
   \item \textbf{Definition (Compatible paths).} ``$\pi_j$ is compatible with $\pi_i$ on $\tm$'' iff:
    \[\forall\pi_i'\sqsubseteq\pi_i\text{ s.t. }\HeadOf{\pi_i'[t]} = \HeadOf{t}
    \text{, then }\pi_j[\pi_i'[t]] \neq \Omega.\]
  \item Resta da dimostrare che esista un modo di pre-processare i termini nostri
   e ottenere degli inerti scelti.
\end{itemize}




\clearpage
\section*{Syntactic Condition}

\begin{definition}[Separable]
  Let $t$, $s$ normal terms.

  They are (semi?) separable iff
  there exists $t' \preceq t$ and $\pi$ s.t. $t'' = \pi[t']$
  S.T. for every $s' \preceq s$ s.t. $s'' = \pi[s']$,
  $t'' <> s''$.
\end{definition}

An occurrence of a bound variable is usable if its head is not stuck.

A head is stuck

\begin{verbatim}
  Ctx[] is stuck (unappicable) if:
   - it is an application and the head variable is stuck
   - it is a garbage
   -

\end{verbatim}

\end{document}
