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 \subparagraph{Syntax}
\r
17 \[\begin{array}{lll}
\r
18 \tm, \tmtwo & \ddef & \var \mid \tm\,\tmtwo \mid \Lam\var \tm\Semi\vec\tm \\
\r
19 n & \ddef & \Lam\var n \Semi \vec n \mid \var\,\vec n \\
\r
21 C & \ddef & \Box \mid C\,\tm \mid \tm\,C \\
\r
22 P & \ddef & \Box \Semi \vec\tm \mid C[\Lam\var P] \Semi \vec\tm \\
\r
23 \tilde P & \ddef & \vec\tm \Comma \Box \Comma \vec\tm \mid \vec\tm \Comma C[\Lam\var P] \Comma \vec\tm \\
\r
26 \subparagraph{Reduction}
\r
27 \[\begin{array}{lll}
\r
28 P[C[(\Lam\var \tm\Semi\vec\tm)\,\tmtwo]] & \Red{}{\var\in \tm\Comma\vec\tm} &
\r
29 P[C[\tm\Subst\var\tmtwo], \vec\tm\Subst\var\tmtwo]\\
\r
30 P[C[(\Lam\var \tm\Semi\vec\tm)\,\tmtwo]] & \Red{}{\var\not\in\tm\Comma\vec\tm} &
\r
31 P[C[\tm] \Semi \vec\tm\Comma\tmtwo]\\
\r
34 \subparagraph{Properties of the calculus:}
\r
36 \item Every term is normalizing iff it is strongly normalizing.
\r
40 \section*{Syntactic Condition}
\r
42 \begin{definition}[Separable]
\r
43 Let $t$, $s$ normal terms.
\r
45 They are (semi?) separable iff
\r
46 there exists $t' \preceq t$ and $\pi$ s.t. $t'' = \pi[t']$
\r
47 S.T. for every $s' \preceq s$ s.t. $s'' = \pi[s']$,
\r
51 An occurrence of a bound variable is usable if its head is not stuck.
\r
56 Ctx[] is stuck (unappicable) if:
\r
57 - it is an application and the head variable is stuck
\r