From: acondolu <andrea.condoluci@unibo.it>
Date: Tue, 29 May 2018 14:01:51 +0000 (+0200)
Subject: Added strong calculus for separation, plus some ac's notes
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=60a31aaf1d97ffa43a0f99abb32fe47fb0af4113;p=fireball-separation.git

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

diff --git a/ac_notes.tex b/ac_notes.tex
new file mode 100644
index 0000000..aa11df8
--- /dev/null
+++ b/ac_notes.tex
@@ -0,0 +1,63 @@
+\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
+
+\subparagraph{Syntax}
+\[\begin{array}{lll}
+  \tm, \tmtwo & \ddef & \var \mid \tm\,\tmtwo \mid \Lam\var \tm\Semi\vec\tm \\
+  n & \ddef & \Lam\var n \Semi \vec n \mid \var\,\vec n \\
+  \\
+  C & \ddef & \Box \mid C\,\tm \mid \tm\,C \\
+  P & \ddef & \Box \Semi \vec\tm \mid C[\Lam\var P] \Semi \vec\tm  \\
+  \tilde 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\Semi\vec\tm)\,\tmtwo]] & \Red{}{\var\in \tm\Comma\vec\tm} &
+   P[C[\tm\Subst\var\tmtwo], \vec\tm\Subst\var\tmtwo]\\
+   P[C[(\Lam\var \tm\Semi\vec\tm)\,\tmtwo]] & \Red{}{\var\not\in\tm\Comma\vec\tm} &
+    P[C[\tm] \Semi \vec\tm\Comma\tmtwo]\\
+\end{array}\]
+
+\subparagraph{Properties of the calculus:}
+\begin{itemize}
+  \item Every term is normalizing iff it is strongly normalizing.
+\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}
diff --git a/ideas.tex b/ideas.tex
deleted file mode 100644
index ccc0e18..0000000
--- a/ideas.tex
+++ /dev/null
@@ -1,17 +0,0 @@
-\documentclass[12pt]{article}
-\usepackage{blindtext}
-\usepackage{enumerate}
-\usepackage{hyperref, bookmark}
-\usepackage{amsmath, amsfonts, amssymb, amsthm}
-\usepackage{xcolor}
-
-\title{Ideas on Strong Separation}
-\author{Andrea Condoluci}
-
-\input{macros}
-\begin{document}
-
-\maketitle
-
-
-\end{document}
diff --git a/macros.tex b/macros.tex
index 4c82f0b..d647af6 100644
--- a/macros.tex
+++ b/macros.tex
@@ -58,3 +58,23 @@
 \newcommand{\Numeral}[1]{\bar{#1}}
 
 \newcommand{\ToFire}[1]{#1{\downarrow}}
+
+
+% from strong_fireballs macros.tex
+\newcommand{\Lam}[1]{\lambda #1.\,}
+
+\newcommand{\hl}[1]{{\underline{#1}}}
+\newcommand{\Esub}[2]{\texttt{[}#2\texttt{/}#1\texttt{]}}
+\newcommand{\Comma}{\texttt{,}}
+\newcommand{\Semi}{\texttt{;}}
+\newcommand{\Subst}[2]{\{#2/#1\}}
+% \newcommand{\Comma}{}
+\newcommand{\tm}{t}
+\newcommand{\tmtwo}{u}
+\newcommand{\tmthree}{s}
+\newcommand{\var}{x}
+\newcommand{\vartwo}{y}
+\newcommand{\varthree}{z}
+\newcommand{\varfour}{w}
+
+\newcommand{\Red}[2]{\xrightarrow{#2}_{#1}}