document monotonic type systems
authorblanchet
Wed May 04 19:47:41 2011 +0200 (2011-05-04)
changeset 42681281cc069282c
parent 42680 b6c27cf04fe9
child 42682 562046fd8e0c
document monotonic type systems
doc-src/Sledgehammer/sledgehammer.tex
     1.1 --- a/doc-src/Sledgehammer/sledgehammer.tex	Wed May 04 19:35:48 2011 +0200
     1.2 +++ b/doc-src/Sledgehammer/sledgehammer.tex	Wed May 04 19:47:41 2011 +0200
     1.3 @@ -553,11 +553,11 @@
     1.4  not be found.
     1.5  
     1.6  \opfalse{full\_types}{partial\_types}
     1.7 -Specifies whether full-type information is encoded in ATP problems. Enabling
     1.8 -this option can prevent the discovery of type-incorrect proofs, but it also
     1.9 -tends to slow down the ATPs significantly. For historical reasons, the default
    1.10 -value of this option can be overridden using the option ``Sledgehammer: Full
    1.11 -Types'' from the ``Isabelle'' menu in Proof General.
    1.12 +Specifies whether full type information is encoded in ATP problems. Enabling
    1.13 +this option prevents the discovery of type-incorrect proofs, but it also tends
    1.14 +to slow down the ATPs significantly. For historical reasons, the default value
    1.15 +of this option can be overridden using the option ``Sledgehammer: Full Types''
    1.16 +from the ``Isabelle'' menu in Proof General.
    1.17  
    1.18  \opfalse{full\_types}{partial\_types}
    1.19  Specifies whether full-type information is encoded in ATP problems. Enabling
    1.20 @@ -608,33 +608,35 @@
    1.21  
    1.22  \item[$\bullet$]
    1.23  \textbf{%
    1.24 +\textit{preds}?,
    1.25 +\textit{mono\_preds}?,
    1.26 +\textit{mangled\_preds}?, \\
    1.27 +\textit{tags}?,
    1.28 +\textit{mono\_tags}?,
    1.29 +\textit{mangled\_tags}?:} \\
    1.30 +The type systems \textit{preds}, \textit{mono\_preds}, \textit{mangled\_preds},
    1.31 +\textit{tags}, \textit{mono\_tags}, and \textit{mangled\_tags} are fully typed
    1.32 +and virtually sound---i.e., except for pathological cases, all found proofs are
    1.33 +type-correct. For each of these, Sledgehammer also provides a just-as-sound
    1.34 +partially typed variant identified by a question mark (?)\ that detects and
    1.35 +erases monotonic types (notably infinite types).
    1.36 +
    1.37 +\item[$\bullet$]
    1.38 +\textbf{%
    1.39  \textit{preds}!,
    1.40  \textit{mono\_preds}!,
    1.41  \textit{mangled\_preds}!, \\
    1.42  \textit{tags}!,
    1.43  \textit{mono\_tags}!,
    1.44  \textit{mangled\_tags}!:} \\
    1.45 -The type systems \textit{preds}, \textit{mono\_preds}, \textit{mangled\_preds},
    1.46 -\textit{tags}, \textit{mono\_tags}, and \textit{mangled\_tags} are fully typed
    1.47 -and virtually sound. For each of these, Sledgehammer also provides a mildly
    1.48 -unsound variant identified by an exclamation mark (!)\ that types only finite
    1.49 -(and hence especially dangerous) types.
    1.50 -
    1.51 -\item[$\bullet$]
    1.52 -\textbf{%
    1.53 -\textit{preds}?,
    1.54 -\textit{mono\_preds}?,
    1.55 -\textit{mangled\_preds}?, \\
    1.56 -\textit{tags}?,
    1.57 -\textit{mono\_tags}?,
    1.58 -\textit{mangled\_tags}?:} \\
    1.59 -If the exclamation mark (!)\ is replaced by an question mark (?),\ the type
    1.60 -systems type only nonmonotonic (and hence especially dangerous) types. Not
    1.61 -implemented yet.
    1.62 +If the question mark (?)\ is replaced by an exclamation mark (!),\ the
    1.63 +translation erases all types except those that are clearly finite (e.g.,
    1.64 +\textit{bool}). This encoding is unsound.
    1.65  
    1.66  \item[$\bullet$] \textbf{\textit{const\_args}:}
    1.67 -Constants are annotated with their types, supplied as extra arguments, to
    1.68 -resolve overloading. Variables are unbounded.
    1.69 +Like for the other sound encodings, constants are annotated with their types to
    1.70 +resolve overloading, but otherwise no type information is encoded. This encoding
    1.71 +is hence less sound than the exclamation mark (!)\ variants described above.
    1.72  
    1.73  \item[$\bullet$] \textbf{\textit{erased}:} No type information is supplied to
    1.74  the ATP. Types are simply erased.