From: acondolu <andrea.condoluci@unibo.it>
Date: Tue, 5 Jun 2018 17:44:05 +0000 (+0200)
Subject: Added file with strong calculus and definition of distinction
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=5ec655b7e016e184901a3cac3c5f25cebf8f2858;p=fireball-separation.git

Added file with strong calculus and definition of distinction
---

diff --git a/notes.tex b/notes.tex
new file mode 100644
index 0000000..15a8851
--- /dev/null
+++ b/notes.tex
@@ -0,0 +1,72 @@
+\documentclass[12pt]{article}
+\usepackage{blindtext}
+\usepackage{enumerate}
+\usepackage{hyperref, bookmark}
+\usepackage{amsmath, amsfonts, amssymb, amsthm}
+\usepackage{xcolor}
+
+\title{Strong Separation}
+% \author{---}
+\date{\vspace{-2em}\today{}}
+
+\input{macros}
+\renewcommand{\Lam}[2]{\lambda#1.\, \{\!\!\{#2\}\!\!\}}
+
+\begin{document}
+
+\maketitle
+
+\section*{The Calculus}
+\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 rules}
+\[\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}
+\begin{itemize}
+  \item Every term is normalizing iff it is strongly normalizing.
+  \item Ogni strategia e' perpetua!
+  \item \ldots
+\end{itemize}
+
+\clearpage
+\section*{Separation}
+\newcommand{\HeadOf}[1]{\operatorname{head}(#1)}
+\newcommand{\FstOf}[1]{\operatorname{fst}(#1)}
+\newcommand{\DegOf}[1]{\operatorname{deg}(#1)}
+\newcommand{\SubtmOf}[2]{#1\preceq #2}
+\begin{itemize}
+  % \item \textbf{$\boldsymbol\sigma$-separation.}
+  %  \textcolor{red}{come definirlo? con le variabili? con i termini?
+  %   problematico in cbv}
+  %  Two terms are $\sigma$-separable iff there exists a substitution
+  %   $\sigma$ such that \textcolor{red}{???}
+  % \item \textbf{Semi-$\boldsymbol\sigma$-separation.}
+  %  Two terms are semi-$\sigma$-separable iff there exists a substitution
+  %   $\sigma$ such that -- in short -- it makes one diverge and the other one converge.
+  % \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.:
+  \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.
+  \end{itemize}
+\end{itemize}
+
+\end{document}