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

Commit 9388811c authored by jfschaefer's avatar jfschaefer

write-up discussion (smglom file structure, one-word example, example sentence)

parent ec4ef56a
morekeywords={ abstract, concrete, resource, interface, instance,
incomplete, of, with, open,
cat, fun, lincat, lin, oper, flags, param
......@@ -35,6 +44,7 @@
......@@ -96,6 +106,53 @@ Also we should look at the Plato
see also ~\url{}
\section{File Structure in \smglom}
\smglom is structured into modules. Each module roughly corresponds to a mathematical
concept. For example, for the \texttt{emptyset} module, we would have:
\item \texttt{emptyset.tex}: The signature file, which defines things like the
empty set and the property of being empty/non-empty.
\item \texttt{}: The abstract \GF grammar. It assigns
categories to the different concepts/words introduced in \texttt{emptyset.tex}.
We would like to be able to generate this file from \texttt{emptyset.tex}.
Currently, we do not know how these categories should look like
(see also section \ref{sec:oneWordEx}).
\item \texttt{emptyset.mmt}: The \mmt declarations of the introduced concepts.
Ideally, we would like to generate these automatically as well.
\item \texttt{emptyset.ll.tex}: The language file for language \texttt{ll}
(could be \texttt{en}, \texttt{de}, ...) provides natural-language descriptions
of the concepts.
\item \texttt{}: The concrete \GF grammar, corresponding to
\texttt{emptyset.ll.tex}. It should be generated from \texttt{emptyset.ll.tex}
and linearize the words using the resource grammar.
We will probably need a separate abstract \GF grammar that defines all the categories
we need.
\section{Case Study: One-word Example\label{sec:oneWordEx}}
We use the word \emph{``number''} as a minimal example.
Our goal is to have a grammar that is as semantic as possible, while still
being able to use \GF's resource grammar.
Our current example looks like this:
\section{Case Study: Definition of Prime Numbers}
To understand the problem better, we consider the following example sentence:
A positive integer $n$ is called prime, iff there is no positive integer $1 < m < n$
with $m \divides n$.
We would like to parse this sentence with \GF (\lstinline[language={}]{p -cat=EN})
and linearize it into \mmt (\lstinline[language={}]{l -cat=MMT}):
$$\forall m:\mathbb{N}.\texttt{prime}(n) \Leftrightarrow
\nexists m : \mathbb{N}. 1 < m < n \land m \divides n$$
\section{Question: How to use \GF for Formulae}
\ednote{I do not know yet}
a minimal example, in which we try to find out how to
represent the word "number"
abstract oneWordExample = {
P1; -- unary predicate, i.e. I -> O
number : P1; -- we consider nouns predicates
--# -path=.:present
concrete oneWordExampleEN of oneWordExample = open SyntaxEng,ParadigmsEng in {
P1 = N; -- problem: Predicates can also be verbs
number = mkN "number";
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