summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/Doc/Codegen/Evaluation.thy

author | blanchet |

Tue Nov 07 15:16:42 2017 +0100 (20 months ago) | |

changeset 67022 | 49309fe530fd |

parent 66453 | cc19f7ca2ed6 |

child 69422 | 472af2d7835d |

permissions | -rw-r--r-- |

more robust parsing for THF proofs (esp. polymorphic Leo-III proofs)

1 theory Evaluation

2 imports Codegen_Basics.Setup

3 begin (*<*)

5 ML \<open>

6 Isabelle_System.mkdirs (File.tmp_path (Path.basic "examples"))

7 \<close> (*>*)

9 section \<open>Evaluation \label{sec:evaluation}\<close>

11 text \<open>

12 Recalling \secref{sec:principle}, code generation turns a system of

13 equations into a program with the \emph{same} equational semantics.

14 As a consequence, this program can be used as a \emph{rewrite

15 engine} for terms: rewriting a term @{term "t"} using a program to a

16 term @{term "t'"} yields the theorems @{prop "t \<equiv> t'"}. This

17 application of code generation in the following is referred to as

18 \emph{evaluation}.

19 \<close>

22 subsection \<open>Evaluation techniques\<close>

24 text \<open>

25 There is a rich palette of evaluation

26 techniques, each comprising different aspects:

28 \begin{description}

30 \item[Expressiveness.] Depending on the extent to which symbolic

31 computation is possible, the class of terms which can be evaluated

32 can be bigger or smaller.

34 \item[Efficiency.] The more machine-near the technique, the

35 faster it is.

37 \item[Trustability.] Techniques which a huge (and also probably

38 more configurable infrastructure) are more fragile and less

39 trustable.

41 \end{description}

42 \<close>

45 subsubsection \<open>The simplifier (@{text simp})\<close>

47 text \<open>

48 The simplest way for evaluation is just using the simplifier with

49 the original code equations of the underlying program. This gives

50 fully symbolic evaluation and highest trustablity, with the usual

51 performance of the simplifier. Note that for operations on abstract

52 datatypes (cf.~\secref{sec:invariant}), the original theorems as

53 given by the users are used, not the modified ones.

54 \<close>

57 subsubsection \<open>Normalization by evaluation (@{text nbe})\<close>

59 text \<open>

60 Normalization by evaluation @{cite "Aehlig-Haftmann-Nipkow:2008:nbe"}

61 provides a comparably fast partially symbolic evaluation which

62 permits also normalization of functions and uninterpreted symbols;

63 the stack of code to be trusted is considerable.

64 \<close>

67 subsubsection \<open>Evaluation in ML (@{text code})\<close>

69 text \<open>

70 Considerable performance can be achieved using evaluation in ML, at the cost

71 of being restricted to ground results and a layered stack of code to

72 be trusted, including a user's specific code generator setup.

74 Evaluation is carried out in a target language \emph{Eval} which

75 inherits from \emph{SML} but for convenience uses parts of the

76 Isabelle runtime environment. Hence soundness depends crucially

77 on the correctness of the code generator setup; this is one of the

78 reasons why you should not use adaptation (see \secref{sec:adaptation})

79 frivolously.

80 \<close>

83 subsection \<open>Dynamic evaluation\<close>

85 text \<open>

86 Dynamic evaluation takes the code generator configuration \qt{as it

87 is} at the point where evaluation is issued and computes

88 a corresponding result. Best example is the

89 @{command_def value} command for ad-hoc evaluation of

90 terms:

91 \<close>

93 value %quote "42 / (12 :: rat)"

95 text \<open>

96 \noindent @{command value} tries first to evaluate using ML, falling

97 back to normalization by evaluation if this fails.

99 A particular technique may be specified in square brackets, e.g.

100 \<close>

102 value %quote [nbe] "42 / (12 :: rat)"

104 text \<open>

105 To employ dynamic evaluation in documents, there is also

106 a @{text value} antiquotation with the same evaluation techniques

107 as @{command value}.

108 \<close>

111 subsubsection \<open>Term reconstruction in ML\<close>

113 text \<open>

114 Results from evaluation in ML must be

115 turned into Isabelle's internal term representation again. Since

116 that setup is highly configurable, it is never assumed to be trustable.

117 Hence evaluation in ML provides no full term reconstruction

118 but distinguishes the following kinds:

120 \begin{description}

122 \item[Plain evaluation.] A term is normalized using the vanilla

123 term reconstruction from ML to Isabelle; this is a pragmatic

124 approach for applications which do not need trustability.

126 \item[Property conversion.] Evaluates propositions; since these

127 are monomorphic, the term reconstruction is fixed once and for all

128 and therefore trustable -- in the sense that only the regular

129 code generator setup has to be trusted, without relying

130 on term reconstruction from ML to Isabelle.

132 \end{description}

134 \noindent The different degree of trustability is also manifest in the

135 types of the corresponding ML functions: plain evaluation

136 operates on uncertified terms, whereas property conversion

137 operates on certified terms.

138 \<close>

141 subsubsection \<open>The partiality principle \label{sec:partiality_principle}\<close>

143 text \<open>

144 During evaluation exceptions indicating a pattern

145 match failure or a non-implemented function are treated specially:

146 as sketched in \secref{sec:partiality}, such

147 exceptions can be interpreted as partiality. For plain evaluation,

148 the result hence is optional; property conversion falls back

149 to reflexivity in such cases.

150 \<close>

153 subsubsection \<open>Schematic overview\<close>

155 text \<open>

156 \newcommand{\ttsize}{\fontsize{5.8pt}{8pt}\selectfont}

157 \fontsize{9pt}{12pt}\selectfont

158 \begin{tabular}{l||c|c|c}

159 & @{text simp} & @{text nbe} & @{text code} \tabularnewline \hline \hline

160 interactive evaluation & @{command value} @{text "[simp]"} & @{command value} @{text "[nbe]"} & @{command value} @{text "[code]"} \tabularnewline

161 plain evaluation & & & \ttsize@{ML "Code_Evaluation.dynamic_value"} \tabularnewline \hline

162 evaluation method & @{method code_simp} & @{method normalization} & @{method eval} \tabularnewline

163 property conversion & & & \ttsize@{ML "Code_Runtime.dynamic_holds_conv"} \tabularnewline \hline

164 conversion & \ttsize@{ML "Code_Simp.dynamic_conv"} & \ttsize@{ML "Nbe.dynamic_conv"}

165 \end{tabular}

166 \<close>

169 subsection \<open>Static evaluation\<close>

171 text \<open>

172 When implementing proof procedures using evaluation,

173 in most cases the code generator setup is appropriate

174 \qt{as it was} when the proof procedure was written in ML,

175 not an arbitrary later potentially modified setup. This is

176 called static evaluation.

177 \<close>

180 subsubsection \<open>Static evaluation using @{text simp} and @{text nbe}\<close>

182 text \<open>

183 For @{text simp} and @{text nbe} static evaluation can be achieved using

184 @{ML Code_Simp.static_conv} and @{ML Nbe.static_conv}.

185 Note that @{ML Nbe.static_conv} by its very nature

186 requires an invocation of the ML compiler for every call,

187 which can produce significant overhead.

188 \<close>

191 subsubsection \<open>Intimate connection between logic and system runtime\<close>

193 text \<open>

194 Static evaluation for @{text eval} operates differently --

195 the required generated code is inserted directly into an ML

196 block using antiquotations. The idea is that generated

197 code performing static evaluation (called a \<^emph>\<open>computation\<close>)

198 is compiled once and for all such that later calls do not

199 require any invocation of the code generator or the ML

200 compiler at all. This topic deserved a dedicated chapter

201 \secref{sec:computations}.

202 \<close>

204 end