Attention: Maintenance on monday 19.04.2021 from 07:00 - 13:00 (Gitlab and Mattermost are offline!)

Commit c0e3cf0b authored by Michael Kohlhase's avatar Michael Kohlhase

more

parent 2daaecf8
......@@ -51,13 +51,47 @@
\setcounter{tocdepth}{1}\tableofcontents\newpage
\section{Introduction}\label{sec:intro}
We want to extend the \smglom by grammatical information using \GF.
Interesting reads for this are Kevin Kofler's Dissertation~\cite[sections 5 and
We want to extend the \smglom by grammatical information using \GF. Then we can use the
\GF toolchain for language generation from \mmt content, for formalization, and for
translation. The main problem in this is the mathematical lexicon, which we will derive
from the \GF-enhanced \smglom data.
\GF is the ``Grammatical Framework''~\cite{Ranta:GF04,ranta-2011,GF:on}, which seems
uniquely suited for our purposes. It is modular, and it is based (essentially) on LF,
i.e. uses a dependently typed $\lambda$-calculus under the hood.
\section{Using the \GF Grammatical Framework for Mathematics}
Generally \GF grammars have two parts: a \textbf{resource grammar} that has the general
grammar infrastructure (the linguistic categories and operators for the most common
linguistic constructions of a language) and an \textbf{application grammar} that has the
semantic lexicon and idioms. Both again have two parts the \textbf{abstract grammar},
which specifies the abstract syntax trees, and a \textbf{concrete grammar} that has the
linguistic linearizations.
\GF already has resource grammars for all the languages we are going to encounter in
\smglom, so we only have to have come up with application grammars for Math Language.
\begin{compactenum}
\item For the abstract grammar of \smglom, we have to add mathematical types -- which I
have wanted for a long time. I am not quite sure how, but this should be relatively
straightforward using the \mmt syntax: either in the \sTeX signature or just adding an
indenpendent \mmt signature file; we should be able to generate \mmt stubs for that,
after all, we have the symbol files.
\item For the concrete grammar it would be good if we could if we could generate concrete
\GF from the notation definitions. But for the moment, we can just write \GF by hand to
get an overview; again, we should be able to generate stubs.
\end{compactenum}
An interesting read for this are Kevin Kofler's Dissertation~\cite[sections 5 and
6]{Kofler:dgpnml17} and the Master's thesis of Andreas Pichler~\cite{Pichler:srmk16}.
They have already done something similar in the \textsf{Concise}
system/project~\cite{Concise-manual:on}.
\section{Question: How to use \GF for Formulae}
\ednote{I do not know yet}
\section{Conclusion}\label{sec:concl}
\ednote{tbw.}
\printbibliography
\end{document}
......@@ -83,5 +117,6 @@ Interesting reads for this are Kevin Kofler's Dissertation~\cite[sections 5 and
% LocalWords: NNexus organizing organization organizational organizations KohMihSperTes
% LocalWords: datamodel dmsmglom14 defemph contm cmsmglom14 edsmglom14 GinCor KamNed zh
% LocalWords: EncMath Weisstein's Mathworld EisSub wm82 mathhub boxedquote compactdesc
% LocalWords: fbox syno fbox fbox fbox mero nyms hfill rangle es mmtapi nlex infty
% LocalWords: frac1 Wikifiers setcounter tocdepth
% LocalWords: fbox syno fbox fbox fbox mero nyms hfill rangle es mmtapi nlex infty tbw
% LocalWords: frac1 Wikifiers setcounter tocdepth Ranta:GF04,ranta-2011,GF:on
% LocalWords: linearizations Kofler:dgpnml17 Pichler:srmk16
Markdown is supported
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