1 \documentclass[12pt]{article}
\r
2 \usepackage{blindtext}
\r
3 \usepackage{enumerate}
\r
4 \usepackage{hyperref, bookmark}
\r
5 \usepackage{amsmath, amsfonts, amssymb, amsthm}
\r
8 \title{Ideas on Strong Separation}
\r
16 \newcommand{\Prgm}[2]{[#1\Comma #2]}
\r
18 \subparagraph{Syntax}
\r
19 \[\begin{array}{lll}
\r
20 \tm, \tmtwo & \ddef & \var \mid \tm\,\tmtwo \mid \Lam\var \Prgm{\tm}{\vec\tm} \\
\r
21 n & \ddef & \Lam\var \Prgm{n}{\vec n} \mid \var\,\vec n \\
\r
23 C & \ddef & \Box \mid C\,\tm \mid \tm\,C \\
\r
24 P & \ddef & \vec\tm \Comma \Box \Comma \vec\tm \mid \vec\tm \Comma C[\Lam\var P] \Comma \vec\tm \\
\r
27 \subparagraph{Reduction}
\r
28 \[\begin{array}{lll}
\r
29 P[C[(\Lam\var \Prgm\tm{\vec\tm})\,\tmtwo]] & \Red{}{\var\in \Prgm\tm{\vec\tm}} &
\r
30 P[C[\tm\Subst\var\tmtwo]\Comma \vec\tm\Subst\var\tmtwo]\\
\r
31 P[C[(\Lam\var \Prgm\tm{\vec\tm})\,\tmtwo]] & \Red{}{\var\not\in\Prgm\tm{\vec\tm}} &
\r
32 P[C[\tm] \Comma \vec\tm\Comma\tmtwo]\\
\r
35 \subparagraph{Properties of the calculus:}
\r
37 \item Every term is normalizing iff it is strongly normalizing.
\r
38 \item Ogni strategia e' perpetua!
\r
42 \section*{Syntactic Condition}
\r
44 \begin{definition}[Separable]
\r
45 Let $t$, $s$ normal terms.
\r
47 They are (semi?) separable iff
\r
48 there exists $t' \preceq t$ and $\pi$ s.t. $t'' = \pi[t']$
\r
49 S.T. for every $s' \preceq s$ s.t. $s'' = \pi[s']$,
\r
53 An occurrence of a bound variable is usable if its head is not stuck.
\r
58 Ctx[] is stuck (unappicable) if:
\r
59 - it is an application and the head variable is stuck
\r