|
2299
|
1 |
(*<*)
|
|
|
2 |
theory Slides1
|
|
|
3 |
imports "LaTeXsugar" "Nominal"
|
|
|
4 |
begin
|
|
|
5 |
|
|
|
6 |
notation (latex output)
|
|
|
7 |
set ("_") and
|
|
|
8 |
Cons ("_::/_" [66,65] 65)
|
|
|
9 |
|
|
|
10 |
(*>*)
|
|
|
11 |
|
|
|
12 |
|
|
|
13 |
text_raw {*
|
|
|
14 |
\renewcommand{\slidecaption}{TU Munich, 28.~May 2010}
|
|
|
15 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
|
16 |
\mode<presentation>{
|
|
|
17 |
\begin{frame}<1>[t]
|
|
|
18 |
\frametitle{%
|
|
|
19 |
\begin{tabular}{@ {\hspace{-3mm}}c@ {}}
|
|
|
20 |
\\
|
|
|
21 |
\huge Nominal 2\\[-2mm]
|
|
|
22 |
\large Or, How to Reason Conveniently with\\[-5mm]
|
|
|
23 |
\large General Bindings\\[15mm]
|
|
|
24 |
\end{tabular}}
|
|
|
25 |
\begin{center}
|
|
2300
|
26 |
joint work with {\bf Cezary} and Brian Huf\!fman\\[0mm]
|
|
2299
|
27 |
\end{center}
|
|
|
28 |
\end{frame}}
|
|
|
29 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
|
30 |
|
|
|
31 |
*}
|
|
|
32 |
|
|
|
33 |
text_raw {*
|
|
|
34 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
|
35 |
\mode<presentation>{
|
|
2300
|
36 |
\begin{frame}<1-2>
|
|
2299
|
37 |
\frametitle{\begin{tabular}{c}Part I: Nominal Theory\end{tabular}}
|
|
|
38 |
\mbox{}\\[-3mm]
|
|
|
39 |
|
|
2300
|
40 |
\begin{itemize}
|
|
|
41 |
\item sorted atoms and sort-respecting permutations\medskip
|
|
|
42 |
|
|
|
43 |
\onslide<2->{
|
|
|
44 |
\item[] in old Nominal: atoms have dif\!ferent type
|
|
|
45 |
|
|
|
46 |
\begin{center}
|
|
|
47 |
\begin{tabular}{c@ {\hspace{7mm}}c}
|
|
|
48 |
$[] \act c \dn c$ &
|
|
|
49 |
@{text "(a b)::\<pi> \<bullet> c \<equiv>"}
|
|
|
50 |
$\begin{cases}
|
|
|
51 |
\mbox{@{text "b"}} & \text{if} \mbox{@{text "\<pi> \<bullet> c = a"}}\\
|
|
|
52 |
\mbox{@{text "a"}} & \text{if} \mbox{@{text "\<pi> \<bullet> c = b"}}\\
|
|
|
53 |
\mbox{@{text "\<pi> \<bullet> c"}} & \text{otherwise}
|
|
|
54 |
\end{cases}$
|
|
|
55 |
\end{tabular}
|
|
|
56 |
\end{center}}
|
|
|
57 |
\end{itemize}
|
|
2299
|
58 |
|
|
|
59 |
\end{frame}}
|
|
|
60 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
|
61 |
*}
|
|
|
62 |
|
|
|
63 |
text_raw {*
|
|
|
64 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
|
65 |
\mode<presentation>{
|
|
2300
|
66 |
\begin{frame}<1>
|
|
|
67 |
\frametitle{\begin{tabular}{c}Problems\end{tabular}}
|
|
|
68 |
\mbox{}\\[-3mm]
|
|
|
69 |
|
|
|
70 |
\begin{itemize}
|
|
|
71 |
\item $\_ \act \_ :: \alpha perm \Rightarrow \beta \Rightarrow \beta$
|
|
|
72 |
|
|
|
73 |
\item $supp \_ :: \beta \Rightarrow \alpha set$
|
|
|
74 |
|
|
|
75 |
\begin{center}
|
|
|
76 |
$finite (supp x)_{\alpha_1} \ldots finite (supp x)_{\alpha_n}$
|
|
|
77 |
\end{center}
|
|
|
78 |
|
|
|
79 |
\item $\forall \pi_{\alpha_1} \ldots \pi_{\alpha_n}\;.\; P$
|
|
|
80 |
\end{itemize}
|
|
|
81 |
|
|
|
82 |
\end{frame}}
|
|
|
83 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
|
84 |
*}
|
|
|
85 |
|
|
|
86 |
|
|
|
87 |
text_raw {*
|
|
|
88 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
|
89 |
\mode<presentation>{
|
|
2299
|
90 |
\begin{frame}<1>[c]
|
|
|
91 |
\frametitle{\begin{tabular}{c}Part II: General Bindings\end{tabular}}
|
|
|
92 |
\mbox{}\\[-3mm]
|
|
|
93 |
|
|
|
94 |
|
|
|
95 |
\end{frame}}
|
|
|
96 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
|
97 |
*}
|
|
|
98 |
|
|
|
99 |
|
|
|
100 |
|
|
|
101 |
(*<*)
|
|
|
102 |
end
|
|
|
103 |
(*>*) |