report: review Q2

doc/report/applications.tex

@@ -154,36 +154,47 @@ implementations.
     problems with a given property (runtime complexity). We need
     to consider where each of these three components might be stored.
 
-    \textbf{Symbolic Aspect} First, let us consider
+    \textbf{Symbolic and Concrete Aspects} First, let us consider
     algorithms. Algorithms can be formulated as computer code which
-    should be accessible from storage for symbolic knowledge. But
-    symbolic knowledge encodes just the algorithm itself, not what the
-    algorithm is for nor is it possible to quickly evaluate properties
-    such as $NP$~completeness for querying. Such meta data needs to be
-    stored in a separate index.
-
-    \textbf{Organizational Aspect} The purpose of a given algorithm
-    (what problem it solves) as well as meta properties such as time
-    and space complexity needs to be stored in a separate index. For
-    this to be easy to look up, we propose to file this meta
-    information as organizational knowledge. It certainly isn't easily
-    searchable from symbolic or narrative knowledge and nor is it
-    concrete knowledge as we are talking about general properties of
-    algorithms.
-
-    While ULO has a concept of \texttt{ulo:theorem}
-    and \texttt{ulo:proof}, there is no native way to represent
-    (a)~problems (e.g.\ the traveling salesman problem) and
-    (b)~algorithms that compute a given problem. If ULO had such a
-    concept, we could then introduce new data predicates that tell us
-    something about the properties of problems and
-    algorithms. Organized in such a schema, query~$\mathcal{Q}_2$
-    would be easy to service.
-
-    Of course the question here is whether adding another first level
-    concept to ULO is a good idea or whether it would be better to
-    think of another ontology for algorithms. We leave this for later
-    discussion.
+    can be understood as symbolic knowledge (code represented as a
+    syntax tree) or as concrete knowledge (code as text
+    files)~\cites[pp. 8--9]{tetra}{virt}. Either way, we will not be
+    able to query these indices for what problem a given algorithm is
+    solving, nor is it possible to infer properties as complex as
+    $NP$-completeness automatically. Meta data of this kind needs to be
+    stored in a separate index for organizational knowledge, it being
+    the only fit.
+
+    \textbf{Organizational Aspect} If we wish to look up properties
+    about algorithms from organizational knowledge, we first have to
+    think about how to represent this information. We propose to
+    approaches, one using the existing ULO ontology and one that
+    recommends extending ULO to nativly support the concept of
+    algorithms. Both approaches have their distinct trade-offs.
+
+    \textbf{Representing Algorithms} As a first approach, we can try
+    to represent algorithms and problems in terms of existing ULO
+    predicates. As ULO does have a concept of \texttt{theorem} and
+    \texttt{proof}, it might be tempting to exploit the Curry-Howard
+    correspondence and represent algorithms understood as programs in
+    terms of proofs.  But that does not really capture the canonical
+    understanding of algorithms; algorithms are not actually programs,
+    rather there are programs that implement algorithms. Even if we do
+    work around this problem, it is not clear how to represent
+    problems (e.g.\ the traveling salesman problem or the sorting
+    problem) in terms of theorems (propositions, types) that get
+    implemented by a proof (algorithm, program).
+
+    As algorithms make up an important part of certain areas of
+    research, it might be reasonable to introduce native level support
+    for algorithms in ULO or separately in another ontology. An
+    argument for adding support directly to ULO is that ULO aims to be
+    universal and as such should not be without algorithms. An
+    argument for a separate ontology is that what we understand as ULO
+    data sets (Isabelle, Coq) exports already contain triplets from
+    other ontologies (e.g.\ Dublin Core meta data~\cite{dcreport,
+    dcowl}) and keeping concepts separate is not entirely
+    unattractive in itself.
 
     \item \textbf{$\mathcal{Q}_3$ ``Find integer sequences whose
     generating function is a rational polynomial in $\sin(x)$ that has

doc/report/references.bib

@@ -186,3 +186,14 @@
     urldate = {2020-07-07},
     url = {https://gl.mathhub.info/ulo/ulo}
 }
+
+@inproceedings{virt,
+  title={Virtual theories--a uniform interface to mathematical knowledge bases},
+  author={Wiesing, Tom and Kohlhase, Michael and Rabe, Florian},
+  booktitle={International Conference on Mathematical Aspects of Computer and Information Sciences},
+  pages={243--257},
+  year={2017},
+  organization={Springer},
+  url = {https://kwarc.info/people/frabe/Research/WKR_virtual_17.pdf},
+  urldate = {2020-07-09},
+}