Rel.tex

% Formatting
\documentclass{scrartcl}

%% Fixers
\usepackage{fontspec}
\usepackage{realscripts}
\usepackage{xunicode}
\usepackage{polyglossia}

\usepackage[]{microtype}
%% \usepackage[top=0.7in, bottom=0.7in, left=0.6in, right=0.6in]{geometry}
\usepackage[english]{isodate}

% Packages
\usepackage{lastpage}
\usepackage{scrlayer-scrpage}
\usepackage{enumitem}
\usepackage{amsmath}
\usepackage{amssymb}
\usepackage{bussproofs}
\usepackage{stmaryrd}
\usepackage{supertabular}

\usepackage{tikz}
\usepackage{tikz-cd}

%Load Last Fixers

% Settings

\setdefaultlanguage{english}
\setotherlanguage{latin}

\setmainfont{Latin Modern Roman}[Ligatures=TeX,Fractions=On]
\setsansfont{Latin Modern Sans}[Ligatures=TeX,Fractions=On]
\setmonofont{Latin Modern Mono}[Ligatures=TeX,Fractions=On]

%% \hypersetup{bookmarksopen=true,colorlinks=true,allcolors=blue}

%% \setlength{\mathindent}{0pt}

\input{tex/test.tex}

\newcommand{\Rel}{\textbf{Rel}}
\newcommand{\Set}{\textbf{Set}}
\newcommand{\Span}{\textbf{Span}}
\newcommand{\Vect}{\textbf{Vect}}
\newcommand{\Prof}{\textbf{Prof}}
\newcommand{\lk}{\(\bar{\lambda{}}\mu\tilde{\mu}\,\)}

\newcommand{\name}[1]{\LeftLabel{\fbox{#1}}}
\newcommand{\apply}[1]{\RightLabel{\scriptsize{(#1)}}}

\newcommand{\side}[1]{\RightLabel{\scriptsize{\(\left\{#1\right\}\)}}}

\newcommand{\taut}{\AxiomC{\(\top\)}}
\newcommand{\bnfdef}{\mathrel{::=}}

\newcommand{\step}{\mathrel{\rightsquigarrow}}
\newcommand{\with}{\;}
\newcommand{\sat}{\mathbin{\models}}

\def\fCenter{\mathrel{\vdash}}

\newcommand{\axiom}[2]{\fbox{#1}~#2}

%% \newcommand{\axiom}[2]{\begin{prooftree}\name{#1}\AxiomC{\(\top\)}\UnaryInfC{#2}\end{prooftree}}

\DeclareMathOperator{\val}{\textbf{v}}
\DeclareMathOperator{\prd}{\textbf{p}}

\DeclareMathOperator{\unit}{\textbf{I}}
\DeclareMathOperator{\mt}{\emptyset}
\DeclareMathOperator{\coin}{\textbf{!}}
\DeclareMathOperator{\fst}{\pi_1}
\DeclareMathOperator{\snd}{\pi_2}

\DeclareMathOperator{\success}{\textbf{true}}
\newcommand{\pass}{\mathbin{\gg}}

\DeclareMathOperator{\absurd}{\textbf{abort}}
\DeclareMathOperator{\inl}{\textbf{i}_1}
\DeclareMathOperator{\inr}{\textbf{i}_2}

\DeclareMathOperator{\false}{\textbf{false}}
\DeclareMathOperator{\lft}{\textbf{l}}
\DeclareMathOperator{\rgt}{\textbf{r}}

\DeclareMathOperator{\type}{\Box}
\DeclareMathOperator{\prop}{*}
\newcommand{\Type}{\textbf{Type}}

\DeclareMathOperator{\head}{\textbf{h}}
\DeclareMathOperator{\tail}{\textbf{t}}

\newcommand{\Forall}{\lambda{}}

\newcommand{\update}{\mathbin{:=}}

\DeclareMathOperator{\case}{\textbf{m}}

\begin{document}

\title{Internal Language of Rel}
\author{Molly Stewart-Gallus}

\maketitle

I wanted an internal language corresponding to the double category
\Rel{} the double category with sets as objects, relations as
horizontal arrows and functions as vertical arrows.

I present three different calculi: a substructural ``context
calculus'' corresponding to the horizontal edge of \Rel{}; a ``term
calculus'' corresponding to \Set{}, the vertical edge category of
\Rel{}; and a simple ``command calculus'' corresponding to commuting
squares of \Rel{}.

First, I give the basic framework of the calculi. Then I discuss
semantics and applications. And finally I list a few possible
extensions such as coproduct and dependent sum types.

\section*{Core Calculi}

The core context calculus is the linear lambda calculus with a few
symbol changes and corresponds to the closed monoidal structure of the
horizontal edge of \Rel{}.  The core term calculus is a little
language with only product types and corresponds to the Cartesian
structure of \Set{}.  I am still figuring out the core command
calculus which ought to correspond to commuting squares in \Rel{}.

The context calculus has a linear variable rule.  To make
mechanization easier and ensure the typing environment can always be
directly inferred from context expressions linear variables are
explicitly indexed by their types and variable binding is more
imperative.

\subsection*{Grammar, Syntax and Reductions}


\begin{flushleft}
\ottall
\end{flushleft}

\section*{Examples}

%% Technical choices

%% I decided against rules for mapping from \Set{} to \Rel{} because I wanted
%% to see how far \Rel{} could go on its own and also wanted to see if
%% these could be defined later.

\subsection*{Identity}

\( \textbf{id}_t = \lambda{} \mathit{X} \colon t . \mathit{X} \)
{\taut
  \apply{V}
  \UnaryInf$ \bullet , \mathit{X} \colon t \fCenter \mathit{X} \colon t $
  \apply{\(\times\)I}
  \UnaryInf$ \bullet \fCenter \lambda{} X \colon t . \mathit{X} \colon t \otimes t $
  \DisplayProof}
\hfill
{\taut
  \apply{V}
  \UnaryInf$ \bullet , \mathit{X}[N] \fCenter \mathit{X}[N] $
  \apply{\(\times\)I}
  \UnaryInf$ \bullet \fCenter (\lambda{} \mathit{X} \colon t . \mathit{X})[N , N] $
  \DisplayProof}

\subsection*{Composition}

\begin{center}

  \[ f \circ_t g = \lambda{} \mathit{X} \colon t . \, f \, (g \, \mathit{X}) \]

\begin{prooftree}

  \Axiom$ \bullet \fCenter f \colon t_1 \otimes t_2 $

  \Axiom$ \bullet \fCenter g \colon t_0 \otimes t_1 $
  \taut
  \apply{\(\times\)V}
  \UnaryInf$ \bullet , \, X \colon t_0 \fCenter X \colon t_0 $

  \apply{\(\times\)E}
  \BinaryInf$ \bullet , \, X \colon t_0 \fCenter g \, X \colon t_1 $

  \apply{\(\times\)E}
  \BinaryInf$ \bullet , \, X \colon t_0 \fCenter f \, (g \, X) \colon t_2 $
  \apply{\(\times\)I}
  \UnaryInf$ \bullet \fCenter \lambda{} X \colon t_0. \, f \, (g \, X) \colon t_0 \otimes t_2 $

\end{prooftree}

\begin{prooftree}

  \Axiom$ \bullet \fCenter f[N_1, N_2] $

  \Axiom$ \bullet \fCenter g[N_0, N_1] $

  \taut
  \apply{V}
  \UnaryInf$ \bullet , \, X[N_0] \fCenter X[N_0]  $

  \apply{\(\times\)E}
  \BinaryInf$ \bullet , \, X[N_0] \fCenter g \, X [N_1] $

  \apply{\(\times\)E}
  \BinaryInf$ \bullet , \, X[N_0]  \fCenter  f \, (g \, X) [N_2] $
  \apply{\(\times\)I}
  \UnaryInf$ \bullet \fCenter \lambda{} X \colon t_0 . \, f \, (g \, X)  [N_0 , N_2] $
\end{prooftree}

\end{center}

\section*{Categorical Semantics}
%% Useful as hell, cite somewhere ?
%% https://tikzcd.yichuanshen.de/

The intent is to create calculi encoding the core features of the
double category \Rel{}.  If this is successful then terms and types
ought to map to \Rel{} as follows. Note that defining normalization in
terms of closed terms means a little workaround of multisubstition is
required.

\begin{center}

  \begin{align*}
  \Gamma & \vdash v \colon t \\
  \Delta & \vdash E \colon t \\
  & \sigma \colon \Delta \\
  & \rho \colon \Gamma \\
  & [:=\rho]v \Downarrow N
  \end{align*}

  \begin{tikzcd}
    \unit \arrow{dd}[']{\sigma} \arrow[leftrightarrow]{rr}{\textbf{id}} & {} \arrow[Rightarrow,']{dd}{\sigma \vdash E[N]} & \unit  \arrow{d}{\rho} \\
    &                                                                         & \Gamma  \arrow{d}{v}   \\
    \Delta \arrow{rr}[']{E}                           & {}                            & t                   
  \end{tikzcd}
\end{center}

I have no idea about universe issues and such. Dependent sum is probably wrong.

Really need to think about denotation again.

\[
\begin{aligned}
  \llbracket t_0 \times t_1 \rrbracket & =\llbracket t_0 \rrbracket \times \llbracket t_1 \rrbracket \\
  \\
  \llbracket x \rrbracket(\sigma) & = \sigma(x) \\
  \llbracket v_0 , v_1 \rrbracket(\sigma) & =( \llbracket v_0 \rrbracket(\sigma) , \llbracket v_1 \rrbracket(\sigma) ) \\
  \\
  \llbracket X \rrbracket(\sigma, s) & = \sigma(X, s) \\
  \llbracket \coin \rrbracket(\bullet, \coin) & = \top \\
  \llbracket E_0 ; E_1 \rrbracket(\sigma_0 \cup \sigma_1, s) & = \llbracket E_0 \rrbracket(\sigma_0, \coin) \wedge \llbracket E_1 \rrbracket(\sigma_1, s) \\
  \llbracket E_0 , E_1 \rrbracket(\sigma_0 \cup \sigma_1, (s_0 , s_1)) & = \llbracket E_0 \rrbracket(\sigma_0, s_0) \wedge \llbracket E_1 \rrbracket(\sigma_1, s_1) \\
  \llbracket E_0 \, E_1 \rrbracket(\sigma, s_0) & = \exists s_1,  \llbracket E_1 \rrbracket (\sigma, s_1) \wedge \llbracket E_0 \rrbracket (\sigma, (s_1, s_0))\\
  \llbracket \lambda{} X \colon t . E_0 \rrbracket(\sigma, (s_0, s_1)) & = \forall E_1, \llbracket E_1 \rrbracket (\sigma, s_0) \rightarrow \llbracket E_0 \rrbracket ([X \update  s \mapsto \llbracket E_1 \rrbracket(\sigma, s)] \sigma, s_1) 
\end{aligned}
\]

\section*{Applications to Synthetic Category Theory}

A category is a monad in \Span{}.  Once this system has been generalized
to \Span{} we can define monads internal to \Span{}.

This is not fully internal but a simple approach to defining an
equivalence relation might be something like:

\begin{center}

{\axiom{object}{\( \bullet \fCenter O \colon \prop \)}\hfill
\axiom{arrow}{\( \bullet \fCenter R \colon O \times O \)}}

\name{refl}
\Axiom$\bullet \fCenter o \colon O$
\UnaryInf$\bullet \fCenter R[o, o] $
\DisplayProof

\name{trans}
\Axiom$ \bullet \fCenter  \lambda{} \mathit{X} \colon O . R \, (R \, \mathit{X}) [o_0, o_1] $
\side{\bullet \fCenter o_1, o_0 \colon O \times O}
\UnaryInf$ \bullet \fCenter  R [ o_0, o_1 ]$
\DisplayProof

\name{sym}
\Axiom$ \bullet \fCenter  R [ o_0, o_1 ] $
\side{\bullet \fCenter o_1, o_0 \colon O \times O}
\UnaryInf$ \bullet \fCenter  R [ o_1, o_0 ]$
\DisplayProof
      
\end{center}

Generalizing to a constructive interpretation in terms of spans and
groupoids is future work.

\section*{Extensions}

Disjoint union and dependent sum types.

\section*{Disjoint Unions}

Disjoint unions in \Set{} become Cartesian products/coproducts in
\Rel{}.

I have a hunch it is proper for the combination of product/coproduct
to introduce nondeterminism in the operational semantics but I need to
think more about the issue.

\begin{center}

\[\begin{aligned}
& \textbf{Types} & t & \bnfdef \ldots \mid \mt \mid t \oplus t \\
& \textbf{Contexts} & E & \bnfdef \ldots \mid
  \absurd_t E \mid \inl_t E \mid \inr_t E \mid \\
&                     & & \case(E_0, X. E_1, Y. E_2) \mid \false \mid \lft E \mid \rgt E \mid E ; E'  \\
& \textbf{Terms} & v & \bnfdef \ldots \mid \absurd_t v \mid \inl_t v \mid \inr_t v \mid
  \case(v_0, x. v_1, y. v_2)
\end{aligned}\]

\subsubsection*{Context Calculus}

\name{\(\mt\text{E}^\text{T}\)}
\Axiom$\Delta \fCenter E \colon \mt$
\UnaryInf$\Delta \fCenter \absurd_t E \colon t$
\DisplayProof

{\name{\(+\text{I}^\text{T}_1\)}
\Axiom$\Delta \fCenter E \colon t_0$
\UnaryInf$\Delta \fCenter \inl_{t_1} E \colon t_0 \oplus t_1$
\DisplayProof
\hfill
\name{\(+\text{I}^\text{T}_2\)}
\Axiom$\Delta \fCenter E \colon t_1$
\UnaryInf$\Delta \fCenter \inr_{t_0} E \colon t_0 \oplus t_1$
\DisplayProof}

\name{\(+\text{E}^\text{T}\)}
\Axiom$ \Delta \fCenter E_0 \colon t_0 \oplus t_1 $
\Axiom$ \Delta , \, X_0 \colon t_0 \fCenter E_1 \colon t_2 $
\Axiom$ \Delta , \, X_1 \colon t_1 \fCenter E_1 \colon t_2 $
\TrinaryInf$ \Delta \fCenter \case(E_0, x_0. E_1, x_1. E_2) \colon t_2 $
\DisplayProof

\axiom{\(\mt\)I}
      {\( \Delta \fCenter \false \colon \mt \)}

{\name{\(+\text{E}_1\)}
\Axiom$\Delta \fCenter E \colon t_0 \oplus t_1$
\UnaryInf$\Delta \fCenter \lft E \colon t_0$
\DisplayProof
\hfill
\name{\(+\text{E}_2\)}
\Axiom$\Delta \fCenter E \colon t_0 \oplus t_1$
\UnaryInf$\Delta \fCenter \rgt E \colon t_1$
\DisplayProof
}

\name{\(+\)I}
\Axiom$ \Delta \fCenter E_0 \colon t_0 $
\Axiom$ \Delta \fCenter E_1 \colon t_1 $
\BinaryInf$ \Delta \fCenter E_0 ; E_1 \colon t_0 \oplus t_1 $
\DisplayProof

\subsubsection*{Term Calculus}

\name{\(\mt\)E}
\Axiom$\Gamma \fCenter v \colon \mt$
\UnaryInf$\Gamma \fCenter \absurd_t v \colon t$
\DisplayProof

{\name{\(+\text{I}_1\)}
\Axiom$\Gamma \fCenter v \colon t_0$
\UnaryInf$\Gamma \fCenter \inl_{t_1} v \colon t_0 \oplus t_1$
\DisplayProof
\hfill
\name{\(+\text{I}_2\)}
\Axiom$\Gamma \fCenter v \colon t_1$
\UnaryInf$\Gamma \fCenter \inr_{t_0} v \colon t_0 \oplus t_1$
\DisplayProof
}

\name{\(+\)E}
\Axiom$ \Gamma \fCenter v_0 \colon t_0 \oplus t_1 $
\Axiom$ \Gamma , \, x_0 \colon t_0 \fCenter v_1 \colon t_2 $
\Axiom$ \Gamma , \, x_1 \colon t_1 \fCenter v_1 \colon t_2 $
\TrinaryInf$ \Gamma \fCenter \case(v_0, x_0. v_1, x_1. v_2) \colon t_2 $
\DisplayProof

\axiom{\(+\beta_1\)}
      {\( \case(\inl_t(v_0), x_0. v_1, x_1. v_2) \step [x_0 \update v_0] v_1 \)}

\axiom{\(+\beta_2\)}
      {\( \case(\inr_t(v_0), x_0. v_1, x_1. v_2) \step [x_1 \update v_0] v_2 \)}

\subsubsection*{Command Calculus}

{\name{\(+\text{I}_1\)}
\Axiom$\sigma \fCenter E_0 [ N ] $
\UnaryInf$\sigma \fCenter ( E_0 ; E_1 ) [ \inl_t N ]$
\DisplayProof
\hfill
\name{\(+\text{I}_2\)}
\Axiom$\sigma \fCenter  E_1 [ N ]$
\UnaryInf$\sigma \fCenter ( E_0 ; E_1 ) [ \inr_t N] $
\DisplayProof
}

\end{center}

\section*{Dependent Sums}

If product of sets becomes an internal hom in the predicate calculus
then dependent sums ought to become a little like \(\Pi\) types.  So
the predicate calculus effectively becomes like a linear System-F.

Some things become awkward to interpret here though.

I also really can't figure out unpacking. It's messy if you don't want
full dependent types.

Not really good at the typing judgements for dependent sum types.

\begin{center}

\[\begin{aligned}
& \textbf{Types} & t & \bnfdef \ldots \mid x \mid \prop \mid \head(v) \mid \Sigma X \colon \prop . t  \\
& \textbf{Contexts} &  E & \bnfdef \ldots \mid E \, t \mid \lambda{} X \colon \prop . E  \\
& \textbf{Terms} &  v & \bnfdef \ldots \mid \tail(v) \mid \langle x \update t , v \rangle  \\
& \textbf{Command Env} & \sigma & \bnfdef \ldots \mid \Delta , \, X [ t ]
\end{aligned}\]

\subsubsection*{Context Calculus}

\name{\(\Sigma\)E}
\Axiom$ \Delta_0 \fCenter E \colon \Sigma X \colon \prop. t_1 $
\Axiom$ \Delta_1 \fCenter t_0 \colon \prop $
\BinaryInf$ \Delta_0, \, \Delta_1 \fCenter E_0 \, t_0 \colon [X \update t_0] t_1 $
\DisplayProof

\name{\(\Sigma\)I}
\Axiom$ \Delta , \, x \colon \prop \fCenter E \colon t $
\UnaryInf$ \Delta \fCenter \lambda{} X \colon \prop. E \colon \Sigma X \colon \prop . t $
\DisplayProof

\subsubsection*{Term Calculus}

%% \axiom{U}
%%       {\(\Gamma \fCenter U_i \, \Type\)}

%% \name{U}
%% \Axiom$\Gamma \fCenter v \colon U_i$
%% \UnaryInf$\Gamma \fCenter \llbracket v \rrbracket \, \Type$
%% \DisplayProof

%% \axiom{U}
%%       {\(\Gamma \fCenter u_i : U_{i+1} \)}

%% \name{U}
%% \Axiom$\Gamma \fCenter v \colon U_i$
%% \UnaryInf$\Gamma \fCenter \llbracket v \rrbracket \, \Type$
%% \DisplayProof

\name{\(\Sigma\text{E}_1\)}
\Axiom$\Gamma \fCenter E \colon \Sigma x \colon \prop . t$
\UnaryInf$\Gamma \fCenter \head(v) \colon \prop$
\DisplayProof

\name{\(\Sigma\text{E}_2\)}
\Axiom$\Gamma \fCenter v \colon \Sigma x \colon \prop . t$
\UnaryInf$\Gamma \fCenter \tail(v) \colon [x \update \head(v)] t$
\DisplayProof

\name{\(\Sigma\)I}
\Axiom$ \Gamma \fCenter t_0 \colon \prop $
\Axiom$ \Gamma , \, x \colon \prop \fCenter v \colon t_1 $
\BinaryInf$\Gamma \fCenter \langle x \update t_0 , v \rangle \colon \Sigma x \colon \prop. t_0 $
\DisplayProof

{\axiom{\(\Sigma\beta_1\)}{\( \head(\langle x \update t , v \rangle) \step t \)}
\hfill
\axiom{\(\Sigma\beta_2\)}{\( \tail( \langle x \update t , v \rangle) \step [x \update t] v \)}
}

\subsubsection*{Command Calculus}

\name{\(\Sigma\)I}
\Axiom$ \sigma , \,  X [ t ]  \fCenter E [ N ] $
\UnaryInf$ \sigma \fCenter (\lambda{} X \colon \prop . E) [ \langle x \update t , N \rangle ] $
\DisplayProof

\end{center}

I can't figure out commands here at all.

\section*{The Future?}

Satisifies judgments correspond to thin squares. Moving to more
general categories such as \Span{} or \Prof{} or
\Vect{} for matrix math requires an interpretation of squares
carrying constructive content.

\end{document}