applications.tex 2.95 KB
Newer Older
Dennis Müller's avatar
Update    
Dennis Müller committed
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
We have seen how a viewfinder can be used for theory \emph{discovery}. But with minor variations, extensions or more specialized interfaces many other potential use cases open up, which we plan to investigate in the future:
\begin{itemize}
	\item If the codomain of a view is a theory representing a specific model, it would tell her that those
		are \emph{examples} of her abstract theory.
		
		Furthermore, partial views -- especially those that are total on some included theory -- could
		be insightful \emph{counterexamples}.
	
	\item Given that the Viewfinder looks for \emph{partial} views, we can use it to find natural
		extensions of a starting theory. Imagine Jane removing the last of her axioms for ``beautiful sets'' --
		the other axioms (disregarding finitude of her sets) would allow her to find e.g. both Matroids and
		\emph{Ideals}, which would suggest to her to refactor her library accordingly.
		
		Additionally, \emph{surjective} partial views would inform her, that her theory would probably better
		be refactored as an extension of the codomain, which would allow her to use all theorems and definitions
		therein.
		
	\item If we additionally consider views into and out of the theories found, this can make theory discovery even 
		more attractive. For example, a view from a theory of vector spaces intro matroids could inform Jane additionally, 
		that her beautiful sets, being matroids, form a generalization of the notion of linear independence in linear algebra.
		
	\item If we were to keep book on our transfomations during preprocessing and normalization, we could use the found
		views for translating both into the codomain as well as back from there into our starting theory.
		
		This would allow for e.g. discovering and importing theorems and useful definitions from some other library -- 
		which on the basis of our encodings can be done directly by the viewfinder.
		
		A useful interface might specifically prioritize views into theories on top of which there are many
		theorems and definitions that have been discovered.
	\item For the last two use cases, it would be advantageous to look for views \emph{into} our working
			theory instead. 
			
			Note that even though the algorithm is in principle symmetric, some aspects often depend
			on the direction -- e.g. how we preprocess the theories,
			which constants we use as starting points or how we treat and evaluate the resulting (partial) views.
	\item The last example in Section \ref{sec:usecase} shows how we can find properties like commutativity and
		associativity, which can in turn inform a better normalization of the theory, which in turn would potentially
		allow for finding more views. This could iteratively improve the results of the viewfinder.
Michael Kohlhase's avatar
Michael Kohlhase committed
39
40
41
\end{itemize}
%%% Local Variables:
%%% mode: latex
42
%%% eval: (visual-line-mode) (set-fill-column 5000)
Michael Kohlhase's avatar
Michael Kohlhase committed
43
44
%%% TeX-master: "paper"
%%% End:
45
46
47

%  LocalWords:  emph specialized generalization transfomations normalization prioritize
%  LocalWords:  sec:usecase