Added strong calculus for separation, plus some ac's notes

diff --git a/ac_notes.tex b/ac_notes.tex
new file mode 100644 (file)
index 0000000..aa11df8
--- /dev/null
+++ b/ac_notes.tex
@@ -0,0 +1,63 @@
+\documentclass[12pt]{article}\r
+\usepackage{blindtext}\r
+\usepackage{enumerate}\r
+\usepackage{hyperref, bookmark}\r
+\usepackage{amsmath, amsfonts, amssymb, amsthm}\r
+\usepackage{xcolor}\r
+\r
+\title{Ideas on Strong Separation}\r
+\author{Anonymous}\r
+\r
+\input{macros}\r
+\begin{document}\r
+\r
+\maketitle\r
+\r
+\subparagraph{Syntax}\r
+\[\begin{array}{lll}\r
+  \tm, \tmtwo & \ddef & \var \mid \tm\,\tmtwo \mid \Lam\var \tm\Semi\vec\tm \\\r
+  n & \ddef & \Lam\var n \Semi \vec n \mid \var\,\vec n \\\r
+  \\\r
+  C & \ddef & \Box \mid C\,\tm \mid \tm\,C \\\r
+  P & \ddef & \Box \Semi \vec\tm \mid C[\Lam\var P] \Semi \vec\tm  \\\r
+  \tilde P & \ddef & \vec\tm \Comma \Box \Comma \vec\tm \mid \vec\tm \Comma C[\Lam\var P] \Comma \vec\tm  \\\r
+\end{array}\]\r
+\r
+\subparagraph{Reduction}\r
+\[\begin{array}{lll}\r
+  P[C[(\Lam\var \tm\Semi\vec\tm)\,\tmtwo]] & \Red{}{\var\in \tm\Comma\vec\tm} &\r
+   P[C[\tm\Subst\var\tmtwo], \vec\tm\Subst\var\tmtwo]\\\r
+   P[C[(\Lam\var \tm\Semi\vec\tm)\,\tmtwo]] & \Red{}{\var\not\in\tm\Comma\vec\tm} &\r
+    P[C[\tm] \Semi \vec\tm\Comma\tmtwo]\\\r
+\end{array}\]\r
+\r
+\subparagraph{Properties of the calculus:}\r
+\begin{itemize}\r
+  \item Every term is normalizing iff it is strongly normalizing.\r
+\end{itemize}\r
+\r
+\clearpage\r
+\section*{Syntactic Condition}\r
+\r
+\begin{definition}[Separable]\r
+  Let $t$, $s$ normal terms.\r
+\r
+  They are (semi?) separable iff\r
+  there exists $t' \preceq t$ and $\pi$ s.t. $t'' = \pi[t']$\r
+  S.T. for every $s' \preceq s$ s.t. $s'' = \pi[s']$,\r
+  $t'' <> s''$.\r
+\end{definition}\r
+\r
+An occurrence of a bound variable is usable if its head is not stuck.\r
+\r
+A head is stuck\r
+\r
+\begin{verbatim}\r
+  Ctx[] is stuck (unappicable) if:\r
+   - it is an application and the head variable is stuck\r
+   - it is a garbage\r
+   -\r
+\r
+\end{verbatim}\r
+\r
+\end{document}\r

diff --git a/ideas.tex b/ideas.tex
deleted file mode 100644 (file)
index ccc0e18..0000000
--- a/ideas.tex
+++ /dev/null
@@ -1,17 +0,0 @@
-\documentclass[12pt]{article}\r
-\usepackage{blindtext}\r
-\usepackage{enumerate}\r
-\usepackage{hyperref, bookmark}\r
-\usepackage{amsmath, amsfonts, amssymb, amsthm}\r
-\usepackage{xcolor}\r
-\r
-\title{Ideas on Strong Separation}\r
-\author{Andrea Condoluci}\r
-\r
-\input{macros}\r
-\begin{document}\r
-\r
-\maketitle\r
-\r
-\r
-\end{document}\r

diff --git a/macros.tex b/macros.tex
index 4c82f0b94616e233afb851958dfe90963813adec..d647af67476a2bfd61f963778cc5f090651b88be 100644 (file)
--- a/macros.tex
+++ b/macros.tex
@@ -58,3 +58,23 @@
 \newcommand{\Numeral}[1]{\bar{#1}}\r
 \r
 \newcommand{\ToFire}[1]{#1{\downarrow}}\r
+\r
+\r
+% from strong_fireballs macros.tex\r
+\newcommand{\Lam}[1]{\lambda #1.\,}\r
+\r
+\newcommand{\hl}[1]{{\underline{#1}}}\r
+\newcommand{\Esub}[2]{\texttt{[}#2\texttt{/}#1\texttt{]}}\r
+\newcommand{\Comma}{\texttt{,}}\r
+\newcommand{\Semi}{\texttt{;}}\r
+\newcommand{\Subst}[2]{\{#2/#1\}}\r
+% \newcommand{\Comma}{}\r
+\newcommand{\tm}{t}\r
+\newcommand{\tmtwo}{u}\r
+\newcommand{\tmthree}{s}\r
+\newcommand{\var}{x}\r
+\newcommand{\vartwo}{y}\r
+\newcommand{\varthree}{z}\r
+\newcommand{\varfour}{w}\r
+\r
+\newcommand{\Red}[2]{\xrightarrow{#2}_{#1}}\r