Commit 72ba57b8 authored by Dennis Müller's avatar Dennis Müller
Browse files

prelim

parent f0581576
\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}
\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}
%\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\
......
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
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment