From 72ba57b824e25286ec23be8ce7cae6d3ae16c5bd Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Dennis=20M=C3=BCller?= <d.mueller@jacobs-university.de>
Date: Tue, 17 Apr 2018 23:48:49 +0200
Subject: [PATCH] prelim
---
tex/macros.tex | 22 ++++++++++++++++++++++
tex/paper.tex | 4 +++-
tex/prelim.tex | 49 ++++++++++++++++++++++++++++++++++++++++++++++++-
3 files changed, 73 insertions(+), 2 deletions(-)
create mode 100644 tex/macros.tex
diff --git a/tex/macros.tex b/tex/macros.tex
new file mode 100644
index 0000000..eab355e
--- /dev/null
+++ b/tex/macros.tex
@@ -0,0 +1,22 @@
+\newcommand{\bnf}[1]{{\color{red}#1}}
+\newcommand{\type}{\mathtt{type}}
+\newcommand{\kind}{\mathtt{kind}}
+\newcommand{\self}{\mathtt{self}}
+\newcommand{\judg}[2]{#1 \vdash #2}
+\newcommand{\gjudg}[1]{\judg\Gamma{#1}}
+\newcommand{\tjudg}[2]{\judg{\Theta;#1}{#2}}
+\newcommand{\tgjudg}[1]{\tjudg{\Gamma}{#1}}
+\newcommand{\hastype}[2]{ #1 : #2 }
+\newcommand{\judgeq}[3]{ #1 \equiv #2:#3}
+\newcommand{\judgeqc}[2]{ #1 \rewrites #2}
+\newcommand{\oma}[2]{\ensuremath{@\left( #1, #2 \right)}}
+\newcommand{\ombind}[3]{\ensuremath{\beta\left( #1 \left\{ #2 \right\} #3 \right)}}
+
+\newcommand{\incl}[1]{\mathtt{include}\,#1}
+\newcommand{\gray}[1]{{\color{gray}#1}}
+\newcommand{\red}[1]{{\color{red}#1}}
+
+\newcommand{\cn}[1]{\ensuremath{\mathtt{#1}}}
+\def\defemph{\textbf}
+
+
diff --git a/tex/paper.tex b/tex/paper.tex
index 3f567a3..4d1b2be 100644
--- a/tex/paper.tex
+++ b/tex/paper.tex
@@ -1,7 +1,7 @@
\documentclass[orivec]{llncs}
\usepackage[utf8]{inputenc}
-\usepackage{url}
+\usepackage{url, multirow}
%\usepackage{tipa}
\usepackage{amsmath,amssymb,amstext}
\usepackage{graphicx,stmaryrd,mathabx,MnSymbol,tabularx,mathtools}
@@ -61,6 +61,8 @@
\author{Dennis Müller\inst{1} \and Michael Kohlhase\inst{1}\and Florian Rabe\inst{1,2}}
\institute{Computer Science, FAU Erlangen-N\"urnberg\and LRI, Universit\'e Paris Sud}
+\input{macros}
+
\begin{document}
%\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\
diff --git a/tex/prelim.tex b/tex/prelim.tex
index 6b559dc..0dafe61 100644
--- a/tex/prelim.tex
+++ b/tex/prelim.tex
@@ -1 +1,48 @@
-MMT theories, flat, bla
\ No newline at end of file
+MMT theories, flat, bla
+
+\subsection{MMT Grammar}
+
+For the purposes of this paper, we will work with the (only slightly simplified) grammar given in Figure \ref{fig:mmtgrammar}.
+
+\begin{figure}[ht]\centering\vspace*{-1em}
+ \begin{mdframed}
+ \begin{tabular}{rl@{\quad}l|l}
+ \cn{Thy} $::=$ & $T[:T]=\{ (\cn{Inc})^\ast\ (\cn{Const})^\ast \}$ & Theory & \multirow{2}{*}{Modules} \\
+ \cn{View} $::=$ & $T : T \to T = \{ (\cn{Ass})^\ast \}$ & View & \\ \hline
+ \cn{Const} $::=$ & $C [:t] [=t]$ & Constant Declarations& \multirow{3}{*}{Declarations} \\
+ \cn{Inc} $::=$ & $\incl T$ & Includes & \\
+ \cn{Ass} $::=$ & $C = t$ & Assignments & \\ \hline
+ $\Gamma$ $::=$ & $(x [:t][=t])^\ast$ & Variable Contexts & \multirow{2}{*}{Objects} \\
+ $t$ $::=$ & $x \mid T?C \mid \oma{t}{(t)^+} \mid \ombind{t}{\Gamma}{t} $ & Terms & \\\hline\hline
+ $T$ $::=$ & \cn{String} & Module Names & \multirow{3}{*}{Strings} \\
+ $C$ $::=$ & \cn{String} & Constant Names & \\
+ $x$ $::=$ & \cn{String} & Variable Names & \\
+ \end{tabular}
+ \end{mdframed}\vspace*{-.5em}
+ \caption{The MMT Grammar}\label{fig:mmtgrammar}\label{fig:mmtgrammar}\vspace*{-1em}
+\end{figure}
+
+In more detail:
+\begin{itemize}
+ \item Theories have a module name, an optional \emph{meta-theory} and a body consisting of \emph{includes} of other theories
+ and a list of \emph{constant declarations}.
+ \item Constant declarations have a name and two optional term components; a \emph{type} ($[:t]$), and a \emph{definition} ($[=t]$).
+ \item Views $V : T_1 \to T_2$ have a module name, a domain theory $T_1$, a codomain theory $T_2$ and a body consisting of assignments
+ $C = t$.
+ \item Terms are either
+ \begin{itemize}
+ \item variables $x$,
+ \item symbol references $T?C$ (referencing the constant $C$ in theory $T$),
+ \item applications $\oma{f}{a_1,\ldots,a_n}$ of a term $f$ to a list of arguments $a_1,\ldots,a_n$ or
+ \item binding application $\ombind{f}{x_1[:t_1][=d_1],\ldots,x_n[:t_n][=d_n]}{b}$, where $f$ \emph{binds} the variables
+ $x_1,\ldots,x_n$ in the body $b$ (representing binders such as quantifiers, lambdas, dependent type constructors etc.).
+ \end{itemize}
+\end{itemize}
+The term components of a constant in a theory $T$ may only contain symbol references to constants declared previously in $T$, or that are declared in some theory $T'$ (recursively) included in $T$ (or its meta-theory, which we consider an \emph{include} as well).
+We can eliminate all includes in a theory $T$ by simply copying over the constant declarations in the included theories; we call this process \emph{flattening}. We will often and without loss of generality assume a theory to be \emph{flat} for convenience.
+
+An assignment in a view $V:T_1\to T_2$ is syntactically well-formed if for any assignment $C=t$ contained, $C$ is a constant declared in the flattened domain $T_1$ and $t$ is a syntactically well-formed term in the codomain $T_2$. We call a view \emph{total} if all \emph{undefined} constants in the domain have a corresponding assignment and \emph{partial} otherwise.
+
+\subsection{Theory Graphs and Library Encoding}
+
+OAF?, Meta-Theories, Logical Frameworks / LF, HOAS, Judgments-as-Types
\ No newline at end of file
--
GitLab