glossary.tex 7.17 KB
Newer Older
MARCHE Claude's avatar
MARCHE Claude committed
1
% \newcommand{\why}{\textsc{Why}}
Andrei Paskevich's avatar
Andrei Paskevich committed
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 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256

\newglossaryentry{ident}{
  name={identifier},
  description={
    (type \texttt{Ident.ident}) --- a common type to represent
    a name of an object. Every \gls{tysymbol}, \gls{lsymbol},
    \gls{prsymbol}, \gls{tvsymbol}, \gls{vsymbol}, and
    \gls{theory} has a unique identifier that can be used
    to distinguish it from any other object of the same type.
\glspar
    Every identifier has an associated, possibly non-unique,
    string. To avoid collisions in \gls{prettyprinting} and
    to make the output conform to a given format, various
    \glspl{printer} may \glslink{sanitization}{sanitize}
    identifiers. Identifiers may also bear a \gls{location}
    of their origin and a list of \glspl{label}.
\glspar
    An identifier is \gls{unigen} from a \gls{preid} and
    is suitable for \gls{weakmemo}.
\nopostdesc}
}

\newglossaryentry{label}{
  name={label},
  description={
\nopostdesc}
}

\newglossaryentry{location}{
  name={location},
  description={
\nopostdesc}
}

\newglossaryentry{decl}{
  name={declaration},
  description={(type \texttt{Decl.decl})
\nopostdesc}
}

\newglossaryentry{algtype}{
  name={algebraic type},
  description={
\nopostdesc}
}

\newglossaryentry{constructor}{
  name={constructor},
  description={--- a \gls{lsymbol} introduced in
  an \gls{algtype} \gls{decl}. Can be used in \glspl{pattern}
  and as a usual function symbol.
\nopostdesc}
}

\newglossaryentry{lsymbol}{
  name={logical symbol},
  description={(type \texttt{Term.lsymbol}) --- a type representing
  function and predicate symbols. A logical symbol bears a unique
  \gls{ident} and a type signature, describing what types a symbol
  admits in its arguments.
\glspar
  A logical symbol is \gls{unigen} from a \gls{preid} and
  is suitable for \gls{weakmemo}.
\nopostdesc}
}

\newglossaryentry{preid}{
  name={pre-identifier},
  description={(type \texttt{Ident.preid}) --- a preliminary
  non-unique object used to produce unique \glspl{ident}.
\nopostdesc}
}

\newglossaryentry{prettyprinting}{
  name={pretty-printing},
  description={
\nopostdesc}
}

\newglossaryentry{printer}{
  name={printer},
  description={
\nopostdesc}
}

\newglossaryentry{proposition}{
  name={printer},
  description={
\nopostdesc}
}

\newglossaryentry{prsymbol}{
  name={proposition symbol},
  description={(type \texttt{Decl.prsymbol}) --- a type representing
  \gls{proposition} names. A proposition symbol bears a unique \gls{ident},
  is \gls{unigen} from a \gls{preid}, and is suitable for \gls{weakmemo}.
\nopostdesc}
}

\newglossaryentry{sanitization}{
  name={sanitization},
  description={
\nopostdesc}
}

\newglossaryentry{theory}{
  name={theory},
  description={
\nopostdesc}
}

\newglossaryentry{tvsymbol}{
  name={type variable},
  description={
    (type \texttt{Ty.tvsymbol}) --- a type representing symbols of
    type variables. A type variable bears a unique \gls{ident}
    and is \gls{unigen} from a \gls{preid}.
\nopostdesc}
}

\newglossaryentry{hashcons}{
  name={hash-consed},
  description={
    Objects of a given type are hash-consed whenever (a) every
    two semantically equal objects are also physically equal;
    and (b) contrary to \gls{unigen} objects, one can construct
    an hash-consed object equal to an existing one.
\glspar
    Hash-consed objects provide efficient comparison and hash
    operations and are suitable for \gls{weakmemo}.
\nopostdesc}
}

\newglossaryentry{pattern}{
  name={pattern},
  description={(type \texttt{Term.pattern}) --- objects used
  in pattern-matching expressions. A pattern is built of
  \glspl{constructor} and \glspl{vsymbol} with the help of
  smart constructors guaranteeing that every pattern is well-typed.
\glspar
  Patterns are \gls{hashcons}.
\nopostdesc}
}

\newglossaryentry{type}{
  name={type},
  description={(type \texttt{Ty.ty}) --- a type representing, well,
  types in {\why}. Types are built with the help of smart constructors
  guaranteeing that every type is well-formed.
\glspar
  Types are \gls{hashcons} and suitable for \gls{weakmemo}.
\nopostdesc}
}

\newglossaryentry{term}{
  name={term},
  description={(type \texttt{Term.term}) --- a type of logical terms.
  Every term has a \gls{type}. Terms are built with the help of
  smart constructors guaranteeing that every term is well-typed.
  A term can bear a list of \glspl{label}.
\glspar
  In addition to usual first-order terms, {\why} terms can contain
  if-then-else expressions, let-expressions, and \gls{pattern} matching.
\glspar
  Terms are \gls{hashcons}.
\nopostdesc}
}

\newglossaryentry{formula}{
  name={formula},
  description={(type \texttt{Term.fmla}) --- a type of logical formulas.
  Formulas are built with the help of smart constructors guaranteeing
  that every formula is well-typed. A formula can bear a list of
  \glspl{label}.
\glspar
  In addition to usual first-order formulas, {\why} formulas can contain
  if-then-else expressions, let-expressions, and \gls{pattern} matching.
\glspar
  Formulas are \gls{hashcons}.
\nopostdesc}
}

\newglossaryentry{tysymbol}{
  name={type symbol},
  description={(type \texttt{Ty.tysymbol}) --- a type representing
  \gls{type} constructors. A type symbol bears a unique \gls{ident}
  and an arity, is \gls{unigen} from a \gls{preid}, and
  is suitable for \gls{weakmemo}.
\nopostdesc}
}

\newglossaryentry{unigen}{
  name={uniquely generated},
  description={
    Objects of a given type are uniquely generated whenever every
    newly constructed object is physically and semantically distinct
    from any other value of the same type. For example, \glspl{ident}
    are uniquely generated, while \glspl{preid} or \glspl{term} are not.
\glspar
    Uniquely generated objects usually provide efficient comparison
    and hash operations. Thus, they can be used in \gls{hashcons}
    objects and are suitable for \gls{weakmemo}.
\nopostdesc}
}

\newglossaryentry{vsymbol}{
  name={variable},
  description={(type \texttt{Ty.vsymbol}) --- a type representing
  variable symbols. A variable symbol bears a unique \gls{ident}
  and has an associated \gls{type}.
\glspar
  A variable is \gls{unigen} from a \gls{preid}.
\nopostdesc}
}

\newglossaryentry{weakmemo}{
  name={forgetful memoization},
  description={(module \texttt{Hashweak}) --- memoization technique
  that does not create an additional reference to a key, allowing it
  (and its associated value) to be garbage-collected even while
  the memoization table is still accessible. Forgetful memoization
  is used, in particular, to implement \gls{task} \glspl{trans}:
  the transformation results are memoized, but as soon as the
  original task is garbage-collected, these results can be
  dropped, too.
\glspar
  \Glspl{tysymbol}, \glspl{lsymbol}, \glspl{prsymbol},
  \glspl{type}, \glspl{decl}, \glspl{task}, and \glspl{env}
  can be used as keys in forgetful memoization.
\nopostdesc}
}

\newglossaryentry{trans}{
  name={transformation},
  description={(type \texttt{Trans.trans})
\nopostdesc}
}

\newglossaryentry{task}{
  name={task},
  description={(type \texttt{Task.task})
\nopostdesc}
}

\newglossaryentry{env}{
  name={environment},
  description={(type \texttt{Env.env})
\nopostdesc}
}


\printglossary

\gls{type} \gls{term} \gls{formula} \gls{ident} \gls{weakmemo}
\gls{vsymbol} \gls{unigen} \gls{tysymbol} \gls{pattern}