# source:LTS/DICE2014/unimacro.tex@3467

Last change on this file since 3467 was 3467, checked in by piccolo, 6 years ago

slides

• Property svn:executable set to *
File size: 10.7 KB
Line
1\def\Env{\mathbb Env}
2
3\newcommand{\derl}{\vdash^{\ell}_{\nabla}}
4\newcommand{\ders}{\vdash^{*}_{\nabla}}
5\newcommand{\piv}{\nu_{_{\!\nabla}}}
6\newcommand\COMMENT[1]{}
7\newcommand{\der}{\vdash_{\nabla}}
8\newcommand{\SE}{\mathcal{S}}
9
10
11\def\eqclass#1{{\pmb [} #1 {\pmb ]}_{^{\stackrel{\nabla}{\simeq}}}}
12\def\tuple#1{\langle #1 \rangle}
13%\def\cl#1{\mbox{cl}(#1)}
14%\def\clf#1{\mbox{cl}_{fin}(#1)}
15%\def\eval{\mbox{eval}}
16\def\C{\mathbb{C}}
17\def\lift{\jmath}
18
19
20\def\Coh{\mathcal{C}oh}
21%%%%%%%%%%%%%%%%%%%%%%%%%
22\newcommand{\x}{{\tt x}}
23\newcommand{\y}{{\tt y}}
24\newcommand{\z}{{\tt z}}
25\newcommand{\M}{{\tt M}}
26\newcommand{\N}{{\tt N}}
27\newcommand{\toc}{{\tt p}}
28\newcommand{\compatto}{{\tt d}}
29\def\rank{\mbox{\sc rank}}
30%Simboli per spazi coerenti
31%\def\frownsmile{%
32%\mathrel{\vbox{\hbox{${\frown}$}\vspace{-2ex}\hbox{${\smile}$}\vspace{-.3ex}}}}
33%\def\smilefrown{%
34%\mathrel{\vbox{\hbox{${\smile}$}\vspace{-2ex}\hbox{${\frown}$}\vspace{-.5ex}}}}
35%\def\smilefrown{\asymp}
36\newcommand{\Pbot}{{\pmb{\pmb \perp}}}
37\newcommand{\Ptop}{{\pmb{\pmb \top}}}
38\newcommand{\coer}{ \frownsmile}
39%\newcommand{\clique}{\sqsubseteq}
40\newcommand{\Cl}{\mathcal{C}l}
41\newcommand{\tr}{\hbox{$\mathcal{T}$\hspace{-1mm}\hbox{$r$}}}
42\newcommand{\stapprox}{\sqsubseteq_{S}}
43\newcommand{\extapprox}{\sqsubseteq_{E}}
44\def\subfin{\subseteq_{fin}}
45\newcommand \bibar[1]{\lceil{#1}\rfloor}
46\newcommand \Bibar[1]{\left\lceil{#1}\right\rfloor}
47\newcommand{\fix}{{\tt fix}}
48
49%---------------------------------------------------------
50%      ENVIRONMENTS
51%---------------------------------------------------------
52 \newtheorem{notation}{Notation}[section]
53%\newtheorem{example}[notation]{Example}
54% \newtheorem{remark}[notation]{Remark}
55%   \newtheorem{theorem}[notation]{Theorem}
56%    \newtheorem{corollary}[notation]{Corollary}
57%     \newtheorem{proposition}[notation]{Proposition}
58%      \newtheorem{lemma}[notation]{Lemma}
59%       \newtheorem{definition}[notation]{Definition}
60%       \newtheorem{property}[notation]{Property}
61%          \newtheorem{exercise}[notation]{Exercise}
62
63%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%5
64\def\Vin{{ \Delta}}
65\def \Gomega {{\pmb\surd\Omega}}
66\def \Gxp {{\pmb\surd}}
67
68\def \Lomega {{\pmb\angle\Omega}}
69\def \Lxp {{\pmb\angle}}
70
71\def \LVcbn {\rightarrow_{\Lambda\ell}}
72\def \LVcbns {\rightarrow^*_{\Lambda\ell}}
73\def \LVcbv {\rightarrow_{\Gamma\ell}}
74\def \LVcbvs {\rightarrow^*_{\Gamma\ell}}
75
76\def \can {\rightarrow_{\Xi\ell}}
77\def \cans {\rightarrow^*_{\Xi\ell}}
78\def \Xell {\Xi\ell}
79
80\newcommand\kcan[1]{\stackrel{\hspace{-3mm}#1}{\can}}
81
82\def\evr{\mathcal{E}}
83\def\Uio{{\mathcal{U}^\Vin_\Vout}}
84
85\def\UHio{{\mathcal{U}^\Lambda_{\Lambda\mbox{\tiny-HNF}}}}
86
87
88\def\LLb{L_0}
89\def\LLe{L_1}
90\def\VVb{V_0}
91\def\VVe{V_1}
92
93%\newcommand{\restri}[1]{\hspace{-1,3mm}\upharpoonright_{\rm\!#1}\!}
94
95%%%%%%%%%%%    SISTEMI NUMERICI
96\newcommand{\Zero}{\mbox{\sffamily Zero}}
97\newcommand{\Succ}{\mbox{\sffamily Succ}}
98\newcommand{\Test}{\mbox{\sffamily Test}}
99\newcommand{\Pred}{\mbox{\sffamily Pred}}
100\newcommand{\T}{\mbox{\sffamily T}}
101\newcommand{\F}{\mbox{\sffamily F}}
102
103%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% Ex LUMACRO.tex Precede
104%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
105%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
106%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
107
108\def\FV{\mathrm{FV}}
109\def\nfset{\mbox{-NF}}
110\def\Var{\mathrm{Var}}
111
112\newcommand \dstrategy[1]{\,
113            \makebox[0mm]{\raisebox{2,83mm}{$\hspace{5mm}_{#1}$}}
114                          \raisebox{-0.39mm}{$\hookrightarrow$}}
115\newcommand \ndstrategy[1]{\,
116            \makebox[0mm]{\raisebox{2,5mm}{$\hspace{3mm}_{#1}$}}
117                          \raisebox{-0.35mm}{$\Rightarrow$}}
118
119\def\Bnf{\mathsf{nf_{\!\Lambda}}}
120\def\BOnf{\mathsf{nf_{\!\Lambda \Omega}}}
121\def\args{\mathsf{args}}
122
123
124%\renewcommand\vec[1]{\overrightarrow{#1}}
125%\renewcommand\vec[1]{\overrightarrow{#1\;}}
126\newcommand\repre[1]{\ulcorner #1 \urcorner}
127\def \Vred {\rightarrow_{\Vin}}
128\def \Vequ {=_{\Vin}}
129\def \Vpar {\Rightarrow_{\Vin}}
131\def \Wequ {=_{\Vin}}
132\def \Vdst {\hookrightarrow_{\Vin}}
133%\def \can {\rightarrow_{\Xi}}
134%\def \cans {\rightarrow^*_{\Xi}}
135\def  \canequ {=_\Xi}
136\def \Vsolv {\searrow}
137\def \V {{\bf V}}
138\def \NF {{\bf N }}
139\def \L {{\bf L}}
140\def \O {{\bf O}}
141\def \H {{\bf H}}
142\def \e {{\O\eta}}
143\def\erre{{\scriptsize\textcircled{r}}}
144\def\pipi{{\scriptsize\textcircled{\tiny P}}}
145
146%Warning: gli spazi sono sgnificativi nelle definizioni seguenti
147\def\SubTerm{\mbox{\sffamily SubTerm}}
148%\def\len{\mathsf len}
149\def\Val{\mathsf{Val} }
150\def\Vin{{ \Delta}}
151\def\Win{{\widetilde{{\mathsf V}}}}
152\def\Vout{{\Theta}}
153\def\lambdastar{\lambda^{\!\star}\!}
154
155\def \Vcbn {\rightarrow_{\Lambda}}
156\def \Vcbns {\rightarrow^*_{\Lambda}}
157\def \Vcbv {\rightarrow_{\Gamma}}
158\def \Vcbvs {\rightarrow^*_{\Gamma}}
159\def\exe{\rightarrow^p_\Vin}
160\def\con{\Downarrow_{\Vin, \Vout}}
161\def \lom {\rightarrow_{\Lambda\Omega}}
162\def \leta {\rightarrow_{\eta\Omega}}
163\def \reta {\rightarrow_{\eta}}
164
165
166% Semantica operazionale
167\newcommand{\op}{\Downarrow_{{\bf O}}}
168\newcommand{\h}{\Downarrow_{{\bf H}}}
169\newcommand{\nf}{\Downarrow_{{\bf N}}}
170\newcommand{\opi}{\Downarrow_{{\bf I}}}
171\newcommand{\lazy}{\Downarrow_{{\bf L}}}
172\newcommand{\secd}{\Downarrow_{{\bf V}}}
173\newcommand{\inner}{\Downarrow_I}
175\newcommand{\vu}{\rightarrow_v}
176\newcommand{\vv}{\rightarrow^*_v}
177\newcommand{\vstar}{\rightarrow_v^*}
178\newcommand{\vleft}{\rightarrow_l}
179\newcommand{\vbp}{\Rightarrow_v}
180
181% Sistemi numerici
182%\newcommand{\Zero}{{\bf Zero}}
183%\newcommand{\Succ}{{\bf Succ}}
184%\newcommand{\Test}{{\bf Test}}
185%\newcommand{\Pred}{{\bf Pred}}
186%\newcommand{\T}{{\bf T}}
187%\newcommand{\F}{{\bf F}}
188
189
190% 'Settaggi' globali
191
192% proof  e' un ambiente per dimostrazioni. Fa si' che il testo di
193%        una dimostrazione sia preceduto dalla parola "Proof.",
194%        scritta in corsivo, e che sia seguito dal quadratino di
195%        fine dimostrazione, allineato a destra.
196%        Va tenuto presente che il quadratino di fine dimostrazione
197%        potrebbe comparire, da solo, nella pagina che segue la
198%        dimostrazione, oppure allineato a sinistra, a seconda se,
199%        rispettivamente, la dimostrazione termini a fine pagina o
200%        con una riga larga come tutta la pagina.
201
202%\renewenvironment{proof}{\begin{proof}}{\hfill $\box$ \end{proof}}
203%\renewenvironment{proof}{{\it Proof.} }{\hspace*{\fill}$\Box$\medskip}
204%\renewenvironment{proof}{{\it Proof.} }{\hfill $\Box$\vspace{\baselineskip}}
205%\newenvironment{proof}{\noindent {\em Proof.} }{\hfill $\Box$
206%\vspace{\baselineskip}}
208%\def\endproof{\unskip\nobreak\hspace*{\fill}$\Box$\endtrivlist}
209\def\endproof{{%        set up{
210    \parfillskip=0pt
211    \widowpenalty=10000     % so we dont break the page before \square
212   \displaywidowpenalty=10000  % ditto
213   \finalhyphendemerits=0  % TeXbook exercise 14.32
214  %
215  %                 horizontal
216   \leavevmode             % \nobreak means lines not pages
217   \unskip\nobreak                 % remove previous space or glue
218   \hspace*{\fill}
219   $\Box$%              % the end-of-proof mark
220  %                   vertical \looseness=-1
221  }\endtrivlist}
222
223%\newenvironment{prova}[2]{\vspace{\baselineskip}\noindent {\bf\em #1} ({\it #2})\\ }{\hspace*{\fill}$\blacktriangle$\medskip}
224\newenvironment{subProof}[2]
225{\vspace{\baselineskip}\noindent $\blacktriangledown\vspace{1mm}$ {\bf #1} ({#2}).\par\noindent}
226{\hspace*{\fill}$\blacksquare$\medskip}
227
228
229
230
231%denotational sematics
232%
233\newcommand{\dpap}{\llbracket}%{[\![}
234\newcommand{\dpch}{\rrbracket}%{]\!]}
235
236%den e' la funzione di interpretazione semantica
237\newcommand{\den}[1]{\dpap {#1} \dpch}
238
239%dene e' la funzione di interpretazione semantica in un environment
240\newcommand{\dene}[2]{\dpap {#1} \dpch _{#2}}
241
242%denm e' la funzione di interpretazione semantica
243% in un modello
244\newcommand{\denm}[2]{\dpap {#1} \dpch^{\cal {#2}}}
245
246%denem e' la funzione di interpretazione semantica
247% in un modello e un environment
248\newcommand{\denem}[3]{\dpap {#1} \dpch^{\cal {#2}}_{#3}}
249
250%dm e' l'uguaglianza denotazionale in un dato modello
251\newcommand{\dm}[1]{\sim_{\cal {#1}}}
252
253\def \dom {{\mathbb D}}
254\def \dvin {{\mathbb I}}
255
256%relazione d'ordine per il modello LL
257\newcommand{\sLL}{\trianglelefteq}
258\newcommand{\eqsLL}{\triangleq}
259
260\newcommand{\cl}[1]{\sqsubseteq_{\mathbb {#1}}}
261
262%costruttore di domini
263\def \con {{\bold c}}
264
265% uno e' il termine \lambda x y.x y.
266%\newcommand{\uno}{\mbox{$1\!\!\!$}\raisebox{.28ex}{$1$}}
267\newcommand{\uno}{\mbox{$1\!\!1$}}
268% metalambda, eset e linimpl sono rispett. il metalambda,l'insieme
269%vuoto e l'implicazione lineare.
270%
271%\newcommand{\metalambda}{\mbox{$\lambda\!\!\!$}\raisebox{.28ex}{$\lambda$}}
272\newcommand{\metalambda}{\mbox{$\lambda\hspace{-1,58mm}\lambda$}}
273%\newcommand{\metalambda}{\mathbb{\bblambda}}
274\newcommand{\metax}[2]{\metalambda {#1}\!:\! {#2} \pmb.\,}
275\newcommand{\eset}{\emptyset}
276\newcommand{\linimpl}{\mathrel{-\!\circ}}
277
278\newcommand{\seq}[3]{#1_{#2} , \!\ldots\! , #1_{#3}}
279
280% seqT serve per scrivere sequenze di variabili tipate indicizzate.
281%        E' come 'seq', ma ha quattro parametri dei quali il secondo
282%        denota il tipo (che variera' sugli stessi indici).
283%
284\newcommand{\seqT}[4]{#1_{#3}\!:\!#2_{#3},\!\ldots\!,#1_{#4}\!:\!#2_{#4}}
285
286% seqL e seqTL sono come 'seq' e 'seqT', ma senza le virgole. Sono utili
287%        per le lambda-astrazioni.
288%
289\newcommand{\seqL}[3]{#1_{#2}\!\ldots\!#1_{#3}}
290\newcommand{\seqTL}[4]{#1_{#3}\!:\!#2_{#3}\!\ldots\!#1_{#4}\!:\!#2_{#4}}
291
292% Di seguito sono definiti vari tipi di spazi. Quelli orizzontali sono
293%        utili in modalita' matematica per distanziare una formula
294%        dall'altra (ad es. una premessa dall'altra in una regola).
295%        Quelli verticali distanziano una riga dalla successiva. Sono
296%        utili ad esempio per separare una regola dalla successiva.
297%
298\newcommand{\xspace}{ \makebox[1em]{} }
299\newcommand{\xspaceD}{ \makebox[2em]{} }
300\newcommand{\xspaceT}{ \makebox[3em]{} }
301\newcommand{\xspaceQ}{ \makebox[4em]{} }
302\newcommand{\xspaceC}{ \makebox[5em]{} }
303\newcommand{\xspaceMezzo}{ \makebox[0.5em]{} }
304
305
306
307\def\leqmodel{\setbox0=\hbox{$\sqsubset$}%\,\hbox
308{\raise.2em\copy0\kern-\wd0\kern0.05em\raise-0.3em\hbox
309{{\small$\sim$}}}\,}
310
311%-------------------------------------------------------------------
312% MACROS FOR MAKE RULES OF SYSTEM
313%-------------------------------------------------------------------
314%\newcommand \UN[3] {\prooftree #3 \justifies #2 \using \scriptstyle #1 \endprooftree}
315%\infer[\scriptsize\mbox{\bf (z)}]{\tt \Gamma \vdash {\bf 0}
316%  \triangle \_}{}
317%\newcommand\cal[1]{\mathcal{#1}}
318
319\newcommand \UN[3]{\infer[\scriptsize #1]{#2}{#3}}
320
321%%% Local Variables:
322%%% mode: latex
323%%% TeX-master: "LogicalModel"
324%%% End:
Note: See TracBrowser for help on using the repository browser.