%PDF-1.5 % 4 0 obj << /S /GoTo /D (chapter.1) >> endobj 7 0 obj (Introduction) endobj 8 0 obj << /S /GoTo /D (section.1.1) >> endobj 11 0 obj (Motivation) endobj 12 0 obj << /S /GoTo /D (section.1.2) >> endobj 15 0 obj (Goal) endobj 16 0 obj << /S /GoTo /D (section.1.3) >> endobj 19 0 obj (Related Work) endobj 20 0 obj << /S /GoTo /D (chapter.2) >> endobj 23 0 obj (Language and syntax) endobj 24 0 obj << /S /GoTo /D (section.2.1) >> endobj 27 0 obj (Syntax) endobj 28 0 obj << /S /GoTo /D (section.2.2) >> endobj 31 0 obj (Expressions) endobj 32 0 obj << /S /GoTo /D (section.2.3) >> endobj 35 0 obj (Notation) endobj 36 0 obj << /S /GoTo /D (section.2.4) >> endobj 39 0 obj (Subexpressions) endobj 40 0 obj << /S /GoTo /D (section.2.5) >> endobj 43 0 obj (Free variables) endobj 44 0 obj << /S /GoTo /D (section.2.6) >> endobj 47 0 obj (Substitutions) endobj 48 0 obj << /S /GoTo /D (section.2.7) >> endobj 51 0 obj (Evaluation and equality) endobj 52 0 obj << /S /GoTo /D (chapter.3) >> endobj 55 0 obj (Partial order of expressions ) endobj 56 0 obj << /S /GoTo /D (section.3.1) >> endobj 59 0 obj (Motivation) endobj 60 0 obj << /S /GoTo /D (subsection.3.1.1) >> endobj 63 0 obj (Conservative approximation of possibly divergent expressions) endobj 64 0 obj << /S /GoTo /D (subsection.3.1.2) >> endobj 67 0 obj (Functions with patterns) endobj 68 0 obj << /S /GoTo /D (subsection.3.1.3) >> endobj 71 0 obj (Case expressions) endobj 72 0 obj << /S /GoTo /D (section.3.2) >> endobj 75 0 obj (Idea) endobj 76 0 obj << /S /GoTo /D (subsection.3.2.1) >> endobj 79 0 obj (Extended language) endobj 80 0 obj << /S /GoTo /D (subsection.3.2.2) >> endobj 83 0 obj () endobj 84 0 obj << /S /GoTo /D (subsection.3.2.3) >> endobj 87 0 obj () endobj 88 0 obj << /S /GoTo /D (subsection.3.2.4) >> endobj 91 0 obj (Intuition) endobj 92 0 obj << /S /GoTo /D (section.3.3) >> endobj 95 0 obj (Definition) endobj 96 0 obj << /S /GoTo /D (section.3.4) >> endobj 99 0 obj (Monotonicity and composition rule) endobj 100 0 obj << /S /GoTo /D (chapter.4) >> endobj 103 0 obj (Semantics) endobj 104 0 obj << /S /GoTo /D (section.4.1) >> endobj 107 0 obj (Evaluation) endobj 108 0 obj << /S /GoTo /D (subsection.4.1.1) >> endobj 111 0 obj (Notation) endobj 112 0 obj << /S /GoTo /D (subsection.4.1.2) >> endobj 115 0 obj (Infimum and supremum) endobj 116 0 obj << /S /GoTo /D (section.4.2) >> endobj 119 0 obj (Examples) endobj 120 0 obj << /S /GoTo /D (subsection.4.2.1) >> endobj 123 0 obj (Equality due to semantics) endobj 124 0 obj << /S /GoTo /D (subsection.4.2.2) >> endobj 127 0 obj (Pattern matching) endobj 128 0 obj << /S /GoTo /D (subsection.4.2.3) >> endobj 131 0 obj (Function evaluation) endobj 132 0 obj << /S /GoTo /D (subsection.4.2.4) >> endobj 135 0 obj (Case evaluation) endobj 136 0 obj << /S /GoTo /D (section.4.3) >> endobj 139 0 obj (Relationship to the -calculus) endobj 140 0 obj << /S /GoTo /D (section.4.4) >> endobj 143 0 obj (Normal form) endobj 144 0 obj << /S /GoTo /D (section.4.5) >> endobj 147 0 obj (Multi-argument functions and currying) endobj 148 0 obj << /S /GoTo /D (subsection.4.5.1) >> endobj 151 0 obj (Comparison with naive currying) endobj 152 0 obj << /S /GoTo /D (section.4.6) >> endobj 155 0 obj (Regular methods) endobj 156 0 obj << /S /GoTo /D (subsection.4.6.1) >> endobj 159 0 obj (Examples) endobj 160 0 obj << /S /GoTo /D (subsection.4.6.2) >> endobj 163 0 obj (Evaluation) endobj 164 0 obj << /S /GoTo /D (section.4.7) >> endobj 167 0 obj (Well-formed statements) endobj 168 0 obj << /S /GoTo /D (subsection.4.7.1) >> endobj 171 0 obj (Notation) endobj 172 0 obj << /S /GoTo /D (chapter.5) >> endobj 175 0 obj (Proving statements) endobj 176 0 obj << /S /GoTo /D (section.5.1) >> endobj 179 0 obj (Statements as input and output) endobj 180 0 obj << /S /GoTo /D (section.5.2) >> endobj 183 0 obj (Deduction rules) endobj 184 0 obj << /S /GoTo /D (subsection.5.2.1) >> endobj 187 0 obj (Notation) endobj 188 0 obj << /S /GoTo /D (subsection.5.2.2) >> endobj 191 0 obj (Relation) endobj 192 0 obj << /S /GoTo /D (subsection.5.2.3) >> endobj 195 0 obj (Quantification) endobj 196 0 obj << /S /GoTo /D (subsection.5.2.4) >> endobj 199 0 obj (Admissible) endobj 200 0 obj << /S /GoTo /D (section.5.3) >> endobj 203 0 obj (Promises emitted by successful proofs) endobj 204 0 obj << /S /GoTo /D (subsection.5.3.1) >> endobj 207 0 obj (Motivation) endobj 208 0 obj << /S /GoTo /D (subsection.5.3.2) >> endobj 211 0 obj (Unification using \040and ) endobj 212 0 obj << /S /GoTo /D (subsection.5.3.3) >> endobj 215 0 obj (Summary) endobj 216 0 obj << /S /GoTo /D (subsection.5.3.4) >> endobj 219 0 obj (Examples) endobj 220 0 obj << /S /GoTo /D (subsection.5.3.5) >> endobj 223 0 obj (General approach) endobj 224 0 obj << /S /GoTo /D (section.5.4) >> endobj 227 0 obj (Proving different types of statements) endobj 228 0 obj << /S /GoTo /D (subsection.5.4.1) >> endobj 231 0 obj (Approach) endobj 232 0 obj << /S /GoTo /D (section.5.5) >> endobj 235 0 obj (Examples of true/provable statements) endobj 236 0 obj << /S /GoTo /D (chapter.6) >> endobj 239 0 obj (Algorithm) endobj 240 0 obj << /S /GoTo /D (section.6.1) >> endobj 243 0 obj (Challenges) endobj 244 0 obj << /S /GoTo /D (section.6.2) >> endobj 247 0 obj (Most general output) endobj 248 0 obj << /S /GoTo /D (subsection.6.2.1) >> endobj 251 0 obj (Examples) endobj 252 0 obj << /S /GoTo /D (section.6.3) >> endobj 255 0 obj (Dealing with undecidability) endobj 256 0 obj << /S /GoTo /D (section.6.4) >> endobj 259 0 obj (Formalization of input and output) endobj 260 0 obj << /S /GoTo /D (subsection.6.4.1) >> endobj 263 0 obj (Required features) endobj 264 0 obj << /S /GoTo /D (subsection.6.4.2) >> endobj 267 0 obj (Encoding) endobj 268 0 obj << /S /GoTo /D (section.6.5) >> endobj 271 0 obj (Not losing information) endobj 272 0 obj << /S /GoTo /D (subsection.6.5.1) >> endobj 275 0 obj (Safe deduction rules) endobj 276 0 obj << /S /GoTo /D (subsection.6.5.2) >> endobj 279 0 obj (Consequences) endobj 280 0 obj << /S /GoTo /D (subsection.6.5.3) >> endobj 283 0 obj (Delayed weakening and global restrictions) endobj 284 0 obj << /S /GoTo /D (subsection.6.5.4) >> endobj 287 0 obj (Example) endobj 288 0 obj << /S /GoTo /D (subsection.6.5.5) >> endobj 291 0 obj (Working with global restrictions) endobj 292 0 obj << /S /GoTo /D (section.6.6) >> endobj 295 0 obj (Internal structure) endobj 296 0 obj << /S /GoTo /D (subsection.6.6.1) >> endobj 299 0 obj (Data) endobj 300 0 obj << /S /GoTo /D (subsection.6.6.2) >> endobj 303 0 obj (Proving strategy) endobj 304 0 obj << /S /GoTo /D (section.6.7) >> endobj 307 0 obj (Conservative approximations) endobj 308 0 obj << /S /GoTo /D (section.6.8) >> endobj 311 0 obj (Example of proving) endobj 312 0 obj << /S /GoTo /D (subsection.6.8.1) >> endobj 315 0 obj (Evaluation) endobj 316 0 obj << /S /GoTo /D (subsection.6.8.2) >> endobj 319 0 obj (Check restrictions) endobj 320 0 obj << /S /GoTo /D (section.6.9) >> endobj 323 0 obj (Example of disproving) endobj 324 0 obj << /S /GoTo /D (subsection.6.9.1) >> endobj 327 0 obj (Check restrictions) endobj 328 0 obj << /S /GoTo /D (section.6.10) >> endobj 331 0 obj (Finding rewrite rules) endobj 332 0 obj << /S /GoTo /D (subsection.6.10.1) >> endobj 335 0 obj (Strategy) endobj 336 0 obj << /S /GoTo /D (subsection.6.10.2) >> endobj 339 0 obj (Interpretation of results) endobj 340 0 obj << /S /GoTo /D (subsection.6.10.3) >> endobj 343 0 obj (Relevant output) endobj 344 0 obj << /S /GoTo /D (chapter.7) >> endobj 347 0 obj (Conclusion) endobj 348 0 obj << /S /GoTo /D (section.7.1) >> endobj 351 0 obj (Evaluation) endobj 352 0 obj << /S /GoTo /D (subsection.7.1.1) >> endobj 355 0 obj (Functors) endobj 356 0 obj << /S /GoTo /D (subsection.7.1.2) >> endobj 359 0 obj (-calculus) endobj 360 0 obj << /S /GoTo /D (subsection.7.1.3) >> endobj 363 0 obj (Limitations) endobj 364 0 obj << /S /GoTo /D (section.7.2) >> endobj 367 0 obj (Future Work) endobj 368 0 obj << /S /GoTo /D (chapter.8) >> endobj 371 0 obj (Appendix) endobj 372 0 obj << /S /GoTo /D (section.8.1) >> endobj 375 0 obj (Monotonicity) endobj 376 0 obj << /S /GoTo /D (subsection.8.1.1) >> endobj 379 0 obj (Data constructor) endobj 380 0 obj << /S /GoTo /D (subsection.8.1.2) >> endobj 383 0 obj (Top/Bottom) endobj 384 0 obj << /S /GoTo /D (subsection.8.1.3) >> endobj 387 0 obj (Fixed-point combinator) endobj 388 0 obj << /S /GoTo /D (subsection.8.1.4) >> endobj 391 0 obj (Substitution of a pattern alternative-bound variable) endobj 392 0 obj << /S /GoTo /D (subsection.8.1.5) >> endobj 395 0 obj (Function/Cases containing a single alternative) endobj 396 0 obj << /S /GoTo /D (subsection.8.1.6) >> endobj 399 0 obj (Function/Cases containing multiple alternatives) endobj 400 0 obj << /S /GoTo /D (subsection.8.1.7) >> endobj 403 0 obj (Consequences of allowing alternative's pattern-variables to be bound by other pattern alternatives) endobj 404 0 obj << /S /GoTo /D (section.8.2) >> endobj 407 0 obj (Proofs for admissible rules) endobj 408 0 obj << /S /GoTo /D (subsection.8.2.1) >> endobj 411 0 obj (Lift) endobj 412 0 obj << /S /GoTo /D (subsection.8.2.2) >> endobj 415 0 obj (Fix) endobj 416 0 obj << /S /GoTo /D (subsection.8.2.3) >> endobj 419 0 obj (Weaken\137) endobj 420 0 obj << /S /GoTo /D (subsection.8.2.4) >> endobj 423 0 obj (Combine\1371) endobj 424 0 obj << /S /GoTo /D (subsection.8.2.5) >> endobj 427 0 obj (Combine\1372) endobj 428 0 obj << /S /GoTo /D (subsection.8.2.6) >> endobj 431 0 obj (CaseCombine\137) endobj 432 0 obj << /S /GoTo /D (subsection.8.2.7) >> endobj 435 0 obj (CaseCombine\137) endobj 436 0 obj << /S /GoTo /D (section.8.3) >> endobj 439 0 obj (Proofs for example statements) endobj 440 0 obj << /S /GoTo /D [441 0 R /Fit] >> endobj 444 0 obj << /Length 1235 /Filter /FlateDecode >> stream xڭVMs6WHj\6!큕`SIȞwAE3cYb[PFN7E9C4HI`h<#0EB(N1:N`mL2^ޡT(&8NnaR"$8)aiN6J$V82bC9J]>0Q[ C-eVJYݟ?)tgs+ 1K#KA,k"ɌJ/w<(轝x714Oiv#q