shortened para 2.3
ci/woodpecker/push/build Pipeline was successful
Details
ci/woodpecker/push/build Pipeline was successful
Details
- added ref on eval - reduced blur - fused 3 paras into one by avoiding in-depth explication of the techniques - established link to runtime-testing and the title
This commit is contained in:
parent
26ddfe5b0c
commit
8722b21c3d
|
@ -174,6 +174,28 @@ isbn="978-3-030-79876-5"
|
|||
year={1998},
|
||||
organization={Springer}
|
||||
}
|
||||
|
||||
|
||||
@inproceedings{HaftmannN10,
|
||||
author = {Florian Haftmann and
|
||||
Tobias Nipkow},
|
||||
editor = {Matthias Blume and
|
||||
Naoki Kobayashi and
|
||||
Germ{\'{a}}n Vidal},
|
||||
title = {Code Generation via Higher-Order Rewrite Systems},
|
||||
booktitle = {Functional and Logic Programming, 10th International Symposium, {FLOPS}
|
||||
2010, Sendai, Japan, April 19-21, 2010. Proceedings},
|
||||
series = {Lecture Notes in Computer Science},
|
||||
volume = {6009},
|
||||
pages = {103--117},
|
||||
publisher = {Springer},
|
||||
year = {2010},
|
||||
url = {https://doi.org/10.1007/978-3-642-12251-4\_9},
|
||||
doi = {10.1007/978-3-642-12251-4\_9},
|
||||
timestamp = {Wed, 25 Sep 2019 18:04:25 +0200},
|
||||
biburl = {https://dblp.org/rec/conf/flops/HaftmannN10.bib},
|
||||
bibsource = {dblp computer science bibliography, https://dblp.org}
|
||||
}
|
||||
|
||||
@article{AehligHN12,
|
||||
author = {Klaus Aehlig and
|
||||
|
|
|
@ -406,15 +406,22 @@ types and can therefore be inherited in a subclass.
|
|||
\<close>
|
||||
|
||||
|
||||
subsection\<open>Advanced Evaluation in Isabelle\<close>
|
||||
text\<open>Besides the powerful, but relatively slow rewriting-based proof method
|
||||
\<^theory_text>\<open>simp\<close>, there are basically two other techniques for the evaluation of terms:
|
||||
\<^item> evaluation via reflection into SML (\<^theory_text>\<open>eval\<close>), and
|
||||
subsection\<open>Term-Evaluations in Isabelle\<close>
|
||||
text\<open>Besides the powerful, but relatively slow Isabelle rewriting-based proof method,
|
||||
there are two other techniques for term evaluation:
|
||||
\<^item> evaluation via reflection @{cite "HaftmannN10"} (\<^theory_text>\<open>eval\<close>), and
|
||||
\<^item> normalization by evaluation @{cite "AehligHN12"} (\<^theory_text>\<open>nbe\<close>).\<close>
|
||||
|
||||
text\<open> \<^noindent> The former is based on a nearly one-to-one compilation of HOL-level datatype specifications
|
||||
and function definitions into SML datatypes and functions.
|
||||
The latter technique --- enabling free variables in terms --- uses a generic data-universe
|
||||
enriched by explicit variables. Both techniques are several orders of magnitude more efficient
|
||||
than standard rewriting. \<^dof> uses both to generate code that evaluates invariant and data-integrity
|
||||
checks on-the-fly during editing. For all examples in our library, this form of runtime-testing
|
||||
is sufficiently fast to remain unnoticed by the user.
|
||||
\<close>
|
||||
(*
|
||||
text\<open>
|
||||
The former is based on a nearly one-to-one compilation of datatype specification
|
||||
constructs and recursive function definitions into SML datatypes and functions.
|
||||
The generated code is directly compiled by the underlying SML compiler of the
|
||||
Isabelle platform. This way, pattern-matching becomes natively compiled rather
|
||||
than interpreted as in the matching process of \<^theory_text>\<open>simp\<close>. @{cite "AehligHN12"}
|
||||
|
@ -433,7 +440,7 @@ for ontological classes on the fly during editing, paving the way for both
|
|||
a uniform specification language of ontological data --- namely \<^hol> --- as
|
||||
well as the possibility to \<^emph>\<open>prove\<close> properties over and relations between
|
||||
classes.\<close>
|
||||
|
||||
*)
|
||||
|
||||
section*[invariants::technical,main_author="Some(@{docitem ''nic''}::author)"]
|
||||
\<open>Term-Context Support, Invariants and Queries in DOF\<close>
|
||||
|
|
Loading…
Reference in New Issue