defs.tex

\newcommand{\To}{\Rightarrow}
\newcommand{\inl}{\mathsf{inl}}
\newcommand{\inr}{\mathsf{inr}}
\newcommand{\alt}{\mathrel{\bf \,\mid\,}}


\newcommand{\extlc}{\text{Ext-}\lambda}
\newcommand{\extlcm}{\text{Ext-}\lambda^{-\text{trans}}}
\newcommand{\extlcmm}{\text{Ext-}\lambda^{-\text{trans}-\text{cast}}}
\newcommand{\extlcprime}{\text{Ext-}\lambda'}
\newcommand{\intlc}{\text{Int-}\lambda}
\newcommand{\intlcbisim}{\text{Int$_\approx$-}\lambda}
\newcommand{\erase}[1]{\lfloor {#1} \rfloor}


\newcommand{\uarrowl}{\mathrel{\rotatebox[origin=c]{-30}{$\leftarrowtail$}}}
\newcommand{\uarrowr}{\mathrel{\rotatebox[origin=c]{60}{$\leftarrowtail$}}}
\newcommand{\darrowl}{\mathrel{\rotatebox[origin=c]{30}{$\twoheadleftarrow$}}}
\newcommand{\darrowr}{\mathrel{\rotatebox[origin=c]{120}{$\twoheadleftarrow$}}}
\newcommand{\vuarrow}{\mathrel{\rotatebox[origin=c]{-90}{$\leftarrowtail$}}}
\newcommand{\vdarrow}{\mathrel{\rotatebox[origin=c]{90}{$\twoheadleftarrow$}}}

% Types, terms, and precision 

\newcommand{\dyn}{?}
\newcommand{\nat}{\text{Nat}}
\newcommand{\bool}{\text{Bool}}
\newcommand{\ra}{\rightharpoonup}
\newcommand{\Ret}[1]{\mathsf{Ret\,}{#1}}
\newcommand{\hole}[1]{\bullet \colon {#1}}
\newcommand{\dyntodyn}{\dyn \ra\, \dyn}


\newcommand{\up}[2]{\langle{#2}\uarrowl{#1}\rangle}
\newcommand{\dn}[2]{\langle{#1}\darrowl{#2}\rangle}

\newcommand{\upc}[2]{\text{up}\,{#1}\,{#2}}
\newcommand{\dnc}[2]{\text{dn}\,{#1}\,{#2}}


\newcommand{\ret}{\mathsf{ret}}
\newcommand{\err}{\mho}
\newcommand{\zro}{\textsf{zro}}
\newcommand{\suc}{\textsf{suc}}
\newcommand{\lda}[2]{\lambda {#1} . {#2}}
\newcommand{\injarr}[1]{\textsf{Inj}_\ra ({#1})}
\newcommand{\injnat}[1]{\textsf{Inj}_\text{nat} ({#1})}
\newcommand{\casenat}[4]{\text{Case}_\text{nat} ({#1}) \{ \text{no} \to {#2} \alt \text{nat}({#3}) \to {#4} \}}
\newcommand{\casearr}[4]{\text{Case}_\ra ({#1}) \{ \text{no} \to {#2} \alt \text{fun}({#3}) \to {#4} \}}
\newcommand{\casedyn}[5]{\text{Case}_\Dyn ({#1}) \{ \text{nat}({#2}) \to {#3} \alt \text{fun}({#4}) \to {#5} \}}
\newcommand{\bind}[3]{\text{var } {#1} = {#2} \text{ in } {#3}}
\newcommand{\matchnat}[4]{\text{match } {#1} \text{ with } \{ \textsf {zero} \Rightarrow {#2} \alt \textsf{ suc } {#3} \Rightarrow {#4} \}}

\newcommand{\refl}{\text{refl}}

\newcommand{\Lift}{\text{Lift}}

%\newcommand{\rel}{\circ\hspace{-4px}-\hspace{-4px}\bullet}
\newcommand{\rel}{\mathrel{\circ\mkern-6mu-\mkern-6mu\bullet}}
\newcommand{\ltdyn}{\sqsubseteq}
\newcommand{\gtdyn}{\sqsupseteq}
\newcommand{\equidyn}{\mathrel{\gtdyn\ltdyn}}
\newcommand{\gamlt}{\Gamma^\ltdyn}
\newcommand{\deltalt}{\Delta^\ltdyn}
\newcommand{\relcomp}{\odot}

\newcommand{\hasty}[3]{{#1} \vdash {#2} \colon {#3}}
\newcommand{\vhasty}[3]{{#1} \vdash^v {#2} \colon {#3}}
\newcommand{\phasty}[3]{{#1} \vdash^c {#2} \colon {#3}}
\newcommand{\etmprec}[4]{{#1} \vdash {#2} \ltdyn_e {#3} \colon {#4}}
\newcommand{\itmprec}[4]{{#1} \vdash {#2} \ltdyn_i {#3} \colon {#4}}
\newcommand{\etmequidyn}[4]{{#1} \vdash {#2} \equidyn_e {#3} \colon {#4}}
\newcommand{\itmequidyn}[4]{{#1} \vdash {#2} \equidyn_i {#3} \colon {#4}}
\newcommand{\synbisim}{\approx_{\text{syn}}}

\newcommand{\Dwn}{\Downarrow}
\newcommand{\qte}[1]{\text{quote}({#1})}

\newcommand{\elab}[1]{\text{Elab}({#1})}

% Perturbations
\newcommand{\pertp}{\text{Pert}^\text{P}}
\newcommand{\perte}{\text{Pert}^\text{E}}
\newcommand{\pertdyn}[2]{\text{pert-dyn}({#1}, {#2})}
\newcommand{\delaypert}[1]{\text{delay-pert}({#1})}

\newcommand{\pertc}{\text{Pert}_{\text{C}}}
\newcommand{\pertv}{\text{Pert}_{\text{V}}}


% SGDT and Intensional Stuff

\newcommand{\later}{\vartriangleright}
\newcommand{\type}{\texttt{Type}}
\newcommand{\lob}{\text{L\"{o}b}}
\newcommand{\tick}{\mathsf{tick}}
\newcommand{\nxt}{\mathsf{next}}
\newcommand{\fix}{\mathsf{fix}}
\newcommand{\kpa}{\kappa}

% Model-related stuff
\newcommand{\calC}{\mathcal{C}}
\newcommand{\Set}{\mathsf{Set}}
\newcommand{\Yo}{\mathsf{Yo}}
\newcommand{\Hom}{\mathsf{Hom}}
\newcommand{\calS}{\mathcal{S}}
\newcommand{\gfix}{\texttt{gfix}}
\newcommand{\calU}{\mathcal{U}}
\newcommand{\laterhat}{\widehat{\later}}
\newcommand{\El}{\mathsf{El}}
\newcommand{\Clock}{\mathsf{Clock}}

\newcommand{\Machine}[1]{\mathsf{Machine}\, {#1}}


% Predomains and EP pairs
\newcommand{\Nat}{\mathsf{Nat}}
\newcommand{\Dyn}{\mathsf{Dyn}}
\newcommand{\ty}[1]{\langle {#1} \rangle}
\newcommand{\li}{L_\mho}
\newcommand{\liclk}[1]{L_\mho [{#1}]}

\newcommand{\ext}[2]{\text{ext}\,{#1}\,{#2}}
\newcommand{\map}[2]{\text{map}\,{#1}\,{#2}}

\newcommand{\ltls}{\lesssim}
\newcommand{\bisim}{\approx}
\newcommand{\semlt}{\le}
\newcommand{\semltbad}{\lesssim}

%\newcommand{\injarr}{\textsf{Inj}_\to}
%\newcommand{\injnat}{\textsf{Inj}_\mathbb{N}}

\newcommand{\id}{\mathsf{id}}
\newcommand{\ep}{\leadsto}

\newcommand{\emb}[2]{\mathsf{emb}_{#1}({#2})}
\newcommand{\proj}[2]{\mathsf{proj}_{#1}({#2})}

\newcommand{\monto}{\to_m}


% Notation for wait functions
\newcommand{\wre}{w_r^e}
\newcommand{\wle}{w_l^e}
\newcommand{\wrp}{w_r^p}
\newcommand{\wlp}{w_l^p}

\newcommand{\sem}[1]{\llbracket {#1} \rrbracket}
\newcommand{\semgl}[1]{{\sem{#1}}^\text{gl}}


% Denotational model
\newcommand{\ptb}{\text{ptb}}
\newcommand{\push}{\text{push}}
\newcommand{\pull}{\text{pull}}

\newcommand{\upf}{\text{up}}
\newcommand{\dnf}{\text{dn}}