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 \renewcommand{\Lam}[2]{\lambda#1.\, \{\!\!\{#2\}\!\!\}}
\r
18 \subparagraph{Syntax}
\r
19 \[\begin{array}{lll}
\r
20 \tm, \tmtwo & \ddef & \var \mid \tm\,\tmtwo \mid \Lam\var{\tm\Comma\vec\tm} \\
\r
21 n & \ddef & \Lam\var{n\Comma\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{\tm\Comma\vec\tm})\,\tmtwo]] & \Red{}{\var\in \tm,\vec\tm} &
\r
30 P[C[\tm\Subst\var\tmtwo]\Comma \vec\tm\Subst\var\tmtwo]\\
\r
31 P[C[(\Lam\var{\tm\Comma\vec\tm})\,\tmtwo]] & \Red{}{\var\not\in\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 \[ E ::= \Box \mid E\, t \mid t\, E \mid \Lam\var{\vec t\Comma E \Comma \vec t} \]
\r
44 \begin{definition}[Unlockable variable]
\r
45 A variable $\var$ is unlockable in a context $E$ if:
\r
47 \item it is not bound in $E$, or
\r
48 \item $E[\cdot] = E'[\vartwo\, \vec\tm \, (\Lam{\cdots\var\cdots}{\vec\tmtwo \Comma E'[\cdot]\Comma\vec\tmthree})]$
\r
49 and $\vartwo$ is unlockable in $E'$.
\r
53 \begin{lemma}[Elimination of unlockable variables]
\r
54 For every set of terms $\tm_1, \ldots, \tm_n$
\r
55 there exist terms $\tm'_1, \ldots, \tm'_n$
\r
56 without unlockable variables and
\r
57 such that $\tm_i$ is unseparable from $\tm'_i$.
\r
62 I termini hanno gli stessi path, e le variabili unlockable
\r
63 del secondo sono iin path virtuali nel primo
\r
65 Piu' esattamente, hai portato il garbage che vuoi far divergere
\r
70 Transformation removing an unlockable variable bound at position $\pi$:
\r
71 \[\tau_{n::\pi}[\alpha] := \lambda x_1..x_n\,x.\, \alpha\,\vec x\,(\tau_\pi[x])\]
\r
75 Warning! It creates unlockable variables, but in positions whose paths were
\r
79 For every semi-$\sigma$-separable $\tm$ and $\tmtwo$,
\r
80 there exist $\sigma$ s.t $\tm\sigma = \ldots \Comma C[i] \Comma \ldots$
\r
81 and $i \not\preceq \tmtwo\sigma$ (and therefore, $\tm\sigma$ and $\tmtwo\sigma$
\r
82 are semi-$\sigma$-separable by ???).
\r
86 $\tm$ and $\tmtwo$ are semi-$\sigma$-separable if \ldots
\r
90 \newcommand{\HeadOf}[1]{\operatorname{hd}(#1)}
\r
91 \newcommand{\ArityOf}[1]{\operatorname{len}(#1)}
\r
93 \item \textbf{A sufficient condition for separability:}
\r
94 \item \textbf{Goal.} semi-$\sigma$-separating $\tm$ from $\tmtwo$ (both inerts with pacmans/$\Omega$).
\r
95 \item Let $U \defeq \{\tmtwo' \mid \tmtwo'\preceq\tmtwo \land \HeadOf{\tmtwo'}=\HeadOf{\tm}
\r
96 \land \ArityOf{\tmtwo'} \leq \ArityOf{\tm}\} = \{u_1, \ldots, u_N\}$.
\r
97 \item \textbf{Theorem.} The problem is separable if there exist $\pi_1\ldots\pi_N$
\r
98 $\eta$-difference paths between
\r
99 $\tm$ and $\tmtwo_1\ldots\tmtwo_N$ that are pairwise compatible on $\tm$ (note: also between themselves).
\r
100 \item \textbf{Definition ($\eta$-difference path).}
\r
101 \item \textbf{Definition ($\sqsubset$).} Initial fragments of paths
\r
102 \item \textbf{Definition (Compatible paths).} ``$\pi_j$ is compatible with $\pi_i$ on $\tm$'' iff:
\r
103 \[\forall\pi_i'\sqsubseteq\pi_i\text{ s.t. }\HeadOf{\pi_i'[t]} = \HeadOf{t}
\r
104 \text{, then }\pi_j[\pi_i'[t]] \neq \Omega.\]
\r
105 \item Resta da dimostrare che esista un modo di pre-processare i termini nostri
\r
106 e ottenere degli inerti scelti.
\r
113 \section*{Syntactic Condition}
\r
115 \begin{definition}[Separable]
\r
116 Let $t$, $s$ normal terms.
\r
118 They are (semi?) separable iff
\r
119 there exists $t' \preceq t$ and $\pi$ s.t. $t'' = \pi[t']$
\r
120 S.T. for every $s' \preceq s$ s.t. $s'' = \pi[s']$,
\r
124 An occurrence of a bound variable is usable if its head is not stuck.
\r
129 Ctx[] is stuck (unappicable) if:
\r
130 - it is an application and the head variable is stuck
\r