comparison src/GeneralRec.v @ 355:62fdf0993e05

Prose for domain-theoretic approach
author Adam Chlipala <adam@chlipala.net>
date Fri, 28 Oct 2011 15:38:41 -0400
parents dc99dffdf20a
children 50e1d338728c
comparison
equal deleted inserted replaced
354:dc99dffdf20a 355:62fdf0993e05
277 Some more recent Coq features provide more convenient syntax for defining recursive functions. Interested readers can consult the Coq manual about the commands %\index{Function}%[Function] and %\index{Program Fixpoint}%[Program Fixpoint]. *) 277 Some more recent Coq features provide more convenient syntax for defining recursive functions. Interested readers can consult the Coq manual about the commands %\index{Function}%[Function] and %\index{Program Fixpoint}%[Program Fixpoint]. *)
278 278
279 279
280 (** * A Non-Termination Monad Inspired by Domain Theory *) 280 (** * A Non-Termination Monad Inspired by Domain Theory *)
281 281
282 (** The key insights of %\index{domain theory}%domain theory%~\cite{WinskelDomains}% inspire the next approach to modeling non-termination. Domain theory is based on %\emph{%#<i>#information orders#</i>#%}% that relate values representing computatiion results, according to how much information these values convey. For instance, a simple domain might include values %``%#"#the program does not terminate#"#%''% and %``%#"#the program terminates with the answer 5.#"#%''% The former is considered to be an %\emph{%#<i>#approximation#</i>#%}% of the latter, while the latter is %\emph{%#<i>#not#</i>#%}% an approximation of %``%#"#the program terminates with the answer 6.#"#%''% The details of domain theory will not be important in what follows; we merely borrow the notion of an approximation ordering on computation results.
283
284 Consider this definition of a type of computations. *)
285
282 Section computation. 286 Section computation.
283 Variable A : Type. 287 Variable A : Type.
288 (** The type [A] describes the result a computation will yield, if it terminates.
289
290 We give a rich dependent type to computations themselves: *)
284 291
285 Definition computation := 292 Definition computation :=
286 {f : nat -> option A 293 {f : nat -> option A
287 | forall (n : nat) (v : A), 294 | forall (n : nat) (v : A),
288 f n = Some v 295 f n = Some v
289 -> forall (n' : nat), n' >= n 296 -> forall (n' : nat), n' >= n
290 -> f n' = Some v}. 297 -> f n' = Some v}.
291 298
299 (** A computation is fundamentally a function [f] from an %\emph{%#<i>#approximation level#</i>#%}% [n] to an optional result. Intuitively, higher [n] values enable termination in more cases than lower values. A call to [f] may return [None] to indicate that [n] was not high enough to run the computation to completion; higher [n] values may yield [Some]. Further, the proof obligation within the sigma type asserts that [f] is %\emph{%#<i>#monotone#</i>#%}% in an appropriate sense: when some [n] is sufficient to produce termination, so are all higher [n] values, and they all yield the same program result [v].
300
301 It is easy to define a relation characterizing when a computation runs to a particular result at a particular approximation level. *)
302
292 Definition runTo (m : computation) (n : nat) (v : A) := 303 Definition runTo (m : computation) (n : nat) (v : A) :=
293 proj1_sig m n = Some v. 304 proj1_sig m n = Some v.
305
306 (** On top of [runTo], we also define [run], which is the most abstract notion of when a computation runs to a value. *)
294 307
295 Definition run (m : computation) (v : A) := 308 Definition run (m : computation) (v : A) :=
296 exists n, runTo m n v. 309 exists n, runTo m n v.
297 End computation. 310 End computation.
311
312 (** The book source code contains at this point some tactics, lemma proofs, and hint commands, to be used in proving facts about computations. Since their details are orthogonal to the message of this chapter, I have omitted them in the rendered version. *)
313 (* begin hide *)
298 314
299 Hint Unfold runTo. 315 Hint Unfold runTo.
300 316
301 Ltac run' := unfold run, runTo in *; try red; crush; 317 Ltac run' := unfold run, runTo in *; try red; crush;
302 repeat (match goal with 318 repeat (match goal with
350 Hint Resolve ge_refl. 366 Hint Resolve ge_refl.
351 367
352 Hint Extern 1 => match goal with 368 Hint Extern 1 => match goal with
353 | [ H : _ = exist _ _ _ |- _ ] => rewrite H 369 | [ H : _ = exist _ _ _ |- _ ] => rewrite H
354 end. 370 end.
371 (* end hide *)
372 (** remove printing exists *)
373
374 (** Now, as a simple first example of a computation, we can define [Bottom], which corresponds to an infinite loop. For any approximation level, it fails to terminate (returns [None]). Note the use of [abstract] to create a new opaque lemma for the proof found by the [run] tactic. In contrast to the previous section, opauqe proofs are fine here, since the proof components of computations do not influence evaluation behavior. *)
355 375
356 Section Bottom. 376 Section Bottom.
357 Variable A : Type. 377 Variable A : Type.
358 378
359 Definition Bottom : computation A. 379 Definition Bottom : computation A.
363 Theorem run_Bottom : forall v, ~run Bottom v. 383 Theorem run_Bottom : forall v, ~run Bottom v.
364 run. 384 run.
365 Qed. 385 Qed.
366 End Bottom. 386 End Bottom.
367 387
388 (** A slightly more complicated example is [Return], which gives the same terminating answer at every approximation level. *)
389
368 Section Return. 390 Section Return.
369 Variable A : Type. 391 Variable A : Type.
370 Variable v : A. 392 Variable v : A.
371 393
372 Definition Return : computation A. 394 Definition Return : computation A.
374 Defined. 396 Defined.
375 397
376 Theorem run_Return : run Return v. 398 Theorem run_Return : run Return v.
377 run. 399 run.
378 Qed. 400 Qed.
379
380 Theorem run_Return_inv : forall x, run Return x -> x = v.
381 run.
382 Qed.
383 End Return. 401 End Return.
384 402
385 Hint Resolve run_Return. 403 (** The name [Return] was meant to be suggestive of the standard operations of monads%~\cite{Monads}%. The other standard operation is [Bind], which lets us run one computation and, if it terminates, pass its result off to another computation. *)
386 404
387 Section Bind. 405 Section Bind.
388 Variables A B : Type. 406 Variables A B : Type.
389 Variable m1 : computation A. 407 Variable m1 : computation A.
390 Variable m2 : A -> computation B. 408 Variable m2 : A -> computation B.
398 let (f2, Hf2) := m2 v in 416 let (f2, Hf2) := m2 v in
399 f2 n 417 f2 n
400 end); abstract run. 418 end); abstract run.
401 Defined. 419 Defined.
402 420
403 Require Import Max.
404
405 Theorem run_Bind : forall (v1 : A) (v2 : B), 421 Theorem run_Bind : forall (v1 : A) (v2 : B),
406 run m1 v1 422 run m1 v1
407 -> run (m2 v1) v2 423 -> run (m2 v1) v2
408 -> run Bind v2. 424 -> run Bind v2.
409 run; match goal with 425 run; match goal with
410 | [ x : nat, y : nat |- _ ] => exists (max x y) 426 | [ x : nat, y : nat |- _ ] => exists (max x y)
411 end; run. 427 end; run.
412 Qed. 428 Qed.
413
414 Theorem run_Bind_inv : forall (v2 : B),
415 run Bind v2
416 -> exists v1 : A,
417 run m1 v1
418 /\ run (m2 v1) v2.
419 run.
420 Qed.
421 End Bind. 429 End Bind.
422 430
423 Hint Resolve run_Bind. 431 (** A simple notation lets us write [Bind] calls the way they appear in Haskell. *)
424 432
425 Notation "x <- m1 ; m2" := 433 Notation "x <- m1 ; m2" :=
426 (Bind m1 (fun x => m2)) (right associativity, at level 70). 434 (Bind m1 (fun x => m2)) (right associativity, at level 70).
435
436 (** We can verify that we have indeed defined a monad, by proving the standard monad laws. Part of the exercise is choosing an appropriate notion of equality between computations. We use %``%#"#equality at all approximation levels.#"#%''% *)
427 437
428 Definition meq A (m1 m2 : computation A) := forall n, proj1_sig m1 n = proj1_sig m2 n. 438 Definition meq A (m1 m2 : computation A) := forall n, proj1_sig m1 n = proj1_sig m2 n.
429 439
430 Theorem left_identity : forall A B (a : A) (f : A -> computation B), 440 Theorem left_identity : forall A B (a : A) (f : A -> computation B),
431 meq (Bind (Return a) f) (f a). 441 meq (Bind (Return a) f) (f a).
440 Theorem associativity : forall A B C (m : computation A) (f : A -> computation B) (g : B -> computation C), 450 Theorem associativity : forall A B C (m : computation A) (f : A -> computation B) (g : B -> computation C),
441 meq (Bind (Bind m f) g) (Bind m (fun x => Bind (f x) g)). 451 meq (Bind (Bind m f) g) (Bind m (fun x => Bind (f x) g)).
442 run. 452 run.
443 Qed. 453 Qed.
444 454
445 Section monotone_runTo. 455 (** Now we come to the piece most directly inspired by domain theory. We want to support general recursive function definitions, but domain theory tells us that not all definitions are reasonable; some fail to be %\emph{%#<i>#continuous#</i>#%}% and thus represent unrealizable computations. To formalize an analogous notion of continuity for our non-termination monad, we write down the approximation relation on computation results that we have had in mind all along. *)
446 Variable A : Type.
447 Variable c : computation A.
448 Variable v : A.
449
450 Theorem monotone_runTo : forall (n1 : nat),
451 runTo c n1 v
452 -> forall n2, n2 >= n1
453 -> runTo c n2 v.
454 run.
455 Qed.
456 End monotone_runTo.
457
458 Hint Resolve monotone_runTo.
459 456
460 Section lattice. 457 Section lattice.
461 Variable A : Type. 458 Variable A : Type.
462 459
463 Definition leq (x y : option A) := 460 Definition leq (x y : option A) :=
464 forall v, x = Some v -> y = Some v. 461 forall v, x = Some v -> y = Some v.
465 End lattice. 462 End lattice.
466 463
467 Hint Unfold leq. 464 (** We now have the tools we need to define a new [Fix] combinator that, unlike the one we saw in the prior section, does not require a termination proof, and in fact admits recursive definition of functions that fail to terminate on some or all inputs. *)
468 465
469 Section Fix. 466 Section Fix.
467 (** First, we have the function domain and range types. *)
468
470 Variables A B : Type. 469 Variables A B : Type.
470
471 (** Next comes the function body, which is written as though it can be parameterized over itself, for recursive calls. *)
472
471 Variable f : (A -> computation B) -> (A -> computation B). 473 Variable f : (A -> computation B) -> (A -> computation B).
474
475 (** Finally, we impose an obligation to prove that the body [f] is continuous. That is, when [f] terminates according to one recursive version of itself, it also terminates with the same result at the same approximation level when passed a recursive version that refines the original, according to [leq]. *)
472 476
473 Hypothesis f_continuous : forall n v v1 x, 477 Hypothesis f_continuous : forall n v v1 x,
474 runTo (f v1 x) n v 478 runTo (f v1 x) n v
475 -> forall (v2 : A -> computation B), 479 -> forall (v2 : A -> computation B),
476 (forall x, leq (proj1_sig (v1 x) n) (proj1_sig (v2 x) n)) 480 (forall x, leq (proj1_sig (v1 x) n) (proj1_sig (v2 x) n))
477 -> runTo (f v2 x) n v. 481 -> runTo (f v2 x) n v.
478 482
483 (** The computational part of the [Fix] combinator is easy to define. At approximation level 0, we diverge; at higher levels, we run the body with a functional argument drawn from the next lower level. *)
484
479 Fixpoint Fix' (n : nat) (x : A) : computation B := 485 Fixpoint Fix' (n : nat) (x : A) : computation B :=
480 match n with 486 match n with
481 | O => Bottom _ 487 | O => Bottom _
482 | S n' => f (Fix' n') x 488 | S n' => f (Fix' n') x
483 end. 489 end.
490
491 (** Now it is straightforward to package [Fix'] as a computation combinator [Fix]. *)
484 492
485 Hint Extern 1 (_ >= _) => omega. 493 Hint Extern 1 (_ >= _) => omega.
486 Hint Unfold leq. 494 Hint Unfold leq.
487 495
488 Lemma Fix'_ok : forall steps n x v, proj1_sig (Fix' n x) steps = Some v 496 Lemma Fix'_ok : forall steps n x v, proj1_sig (Fix' n x) steps = Some v
503 511
504 Definition Fix : A -> computation B. 512 Definition Fix : A -> computation B.
505 intro x; exists (fun n => proj1_sig (Fix' n x) n); abstract run. 513 intro x; exists (fun n => proj1_sig (Fix' n x) n); abstract run.
506 Defined. 514 Defined.
507 515
508 Definition extensional (f : (A -> computation B) -> (A -> computation B)) := 516 (** Finally, we can prove that [Fix] obeys the expected computation rule. *)
509 forall g1 g2 n,
510 (forall x, proj1_sig (g1 x) n = proj1_sig (g2 x) n)
511 -> forall x, proj1_sig (f g1 x) n = proj1_sig (f g2 x) n.
512
513 Hypothesis f_extensional : extensional f.
514 517
515 Theorem run_Fix : forall x v, 518 Theorem run_Fix : forall x v,
516 run (f Fix x) v 519 run (f Fix x) v
517 -> run (Fix x) v. 520 -> run (Fix x) v.
518 run; match goal with 521 run; match goal with
519 | [ n : nat |- _ ] => exists (S n); eauto 522 | [ n : nat |- _ ] => exists (S n); eauto
520 end. 523 end.
521 Qed. 524 Qed.
522 End Fix. 525 End Fix.
523 526
524 Hint Resolve run_Fix. 527 (* begin hide *)
525
526 Lemma leq_Some : forall A (x y : A), leq (Some x) (Some y) 528 Lemma leq_Some : forall A (x y : A), leq (Some x) (Some y)
527 -> x = y. 529 -> x = y.
528 intros ? ? ? H; generalize (H _ (refl_equal _)); crush. 530 intros ? ? ? H; generalize (H _ (refl_equal _)); crush.
529 Qed. 531 Qed.
530 532
531 Lemma leq_None : forall A (x y : A), leq (Some x) None 533 Lemma leq_None : forall A (x y : A), leq (Some x) None
532 -> False. 534 -> False.
533 intros ? ? ? H; generalize (H _ (refl_equal _)); crush. 535 intros ? ? ? H; generalize (H _ (refl_equal _)); crush.
534 Qed. 536 Qed.
537
538 Ltac mergeSort' := run;
539 repeat (match goal with
540 | [ |- context[match ?E with O => _ | S _ => _ end] ] => destruct E
541 end; run);
542 repeat match goal with
543 | [ H : forall x, leq (proj1_sig (?f x) _) (proj1_sig (?g x) _) |- _ ] =>
544 match goal with
545 | [ H1 : f ?arg = _, H2 : g ?arg = _ |- _ ] =>
546 generalize (H arg); rewrite H1; rewrite H2; clear H1 H2; simpl; intro
547 end
548 end; run; repeat match goal with
549 | [ H : _ |- _ ] => (apply leq_None in H; tauto) || (apply leq_Some in H; subst)
550 end; auto.
551 (* end hide *)
552
553 (** After all that work, it is now fairly painless to define a version of [mergeSort] that requires no proof of termination. We appeal to a program-specific tactic whose definition is hidden here but present in the book source. *)
535 554
536 Definition mergeSort' : forall A, (A -> A -> bool) -> list A -> computation (list A). 555 Definition mergeSort' : forall A, (A -> A -> bool) -> list A -> computation (list A).
537 refine (fun A le => Fix 556 refine (fun A le => Fix
538 (fun (mergeSort : list A -> computation (list A)) 557 (fun (mergeSort : list A -> computation (list A))
539 (ls : list A) => 558 (ls : list A) =>
540 if le_lt_dec 2 (length ls) 559 if le_lt_dec 2 (length ls)
541 then let lss := partition ls in 560 then let lss := partition ls in
542 ls1 <- mergeSort (fst lss); 561 ls1 <- mergeSort (fst lss);
543 ls2 <- mergeSort (snd lss); 562 ls2 <- mergeSort (snd lss);
544 Return (merge le ls1 ls2) 563 Return (merge le ls1 ls2)
545 else Return ls) _); abstract (run; 564 else Return ls) _); abstract mergeSort'.
546 repeat (match goal with
547 | [ |- context[match ?E with O => _ | S _ => _ end] ] => destruct E
548 end; run);
549 repeat match goal with
550 | [ H : forall x, leq (proj1_sig (?f x) _) (proj1_sig (?g x) _) |- _ ] =>
551 match goal with
552 | [ H1 : f ?arg = _, H2 : g ?arg = _ |- _ ] =>
553 generalize (H arg); rewrite H1; rewrite H2; clear H1 H2; simpl; intro
554 end
555 end; run; repeat match goal with
556 | [ H : _ |- _ ] => (apply leq_None in H; tauto) || (apply leq_Some in H; subst)
557 end; auto).
558 Defined. 565 Defined.
559 566
560 Print mergeSort'. 567 (** Furthermore, %``%#"#running#"#%''% [mergeSort'] on concrete inputs is as easy as choosing a sufficiently high approximation level and letting Coq's computation rules do the rest. Contrast this with the proof work that goes into deriving an evaluation fact for a deeply embedded language, with one explicit proof rule application per execution step. *)
561 568
562 Lemma test_mergeSort' : run (mergeSort' leb (1 :: 2 :: 36 :: 8 :: 19 :: nil)) 569 Lemma test_mergeSort' : run (mergeSort' leb (1 :: 2 :: 36 :: 8 :: 19 :: nil))
563 (1 :: 2 :: 8 :: 19 :: 36 :: nil). 570 (1 :: 2 :: 8 :: 19 :: 36 :: nil).
564 exists 4; reflexivity. 571 exists 4; reflexivity.
565 Qed. 572 Qed.
566 573
574 (** There is another benefit of our new [Fix] compared with one we used in the previous section: we can now write recursive functions that sometimes fail to terminate, without losing easy reasoning principles for the terminating cases. Consider this simple example, which appeals to another tactic whose definition we elide here. *)
575
576 (* begin hide *)
577 Ltac looper := unfold leq in *; run;
578 repeat match goal with
579 | [ x : unit |- _ ] => destruct x
580 | [ x : bool |- _ ] => destruct x
581 end; auto.
582 (* end hide *)
583
567 Definition looper : bool -> computation unit. 584 Definition looper : bool -> computation unit.
568 refine (Fix (fun looper (b : bool) => 585 refine (Fix (fun looper (b : bool) =>
569 if b then Return tt else looper b) _); 586 if b then Return tt else looper b) _); abstract looper.
570 abstract (unfold leq in *; run;
571 repeat match goal with
572 | [ x : unit |- _ ] => destruct x
573 | [ x : bool |- _ ] => destruct x
574 end; auto).
575 Defined. 587 Defined.
576 588
577 Lemma test_looper : run (looper true) tt. 589 Lemma test_looper : run (looper true) tt.
578 exists 1; reflexivity. 590 exists 1; reflexivity.
579 Qed. 591 Qed.
592
593 (** As before, proving outputs for specific inputs is as easy as demonstrating a high enough approximation level.
594
595 There are other theorems that are important to prove about combinators like [Return], [Bind], and [Fix]. In general, for a computation [c], we sometimes have a hypothesis proving [run c v] for some [v], and we want to perform inversion to deduce what [v] must be. Each combinator should ideally have a theorem of that kind, for [c] built directly from that combinator. We have omitted such theorems here, but they are not hard to prove. In general, the domain theory-inspired approach avoids the type-theoretic %``%#"#gotchas#"#%''% that tend to show up in approaches that try to mix normal Coq computation with explicit syntax types. The next section of this chapter demonstrates two alternate approaches of that sort. *)
580 596
581 597
582 (** * Co-Inductive Non-Termination Monads *) 598 (** * Co-Inductive Non-Termination Monads *)
583 599
584 CoInductive thunk (A : Type) : Type := 600 CoInductive thunk (A : Type) : Type :=
662 intros; rewrite <- (frob_eq (TBind (Answer v) m2)); 678 intros; rewrite <- (frob_eq (TBind (Answer v) m2));
663 simpl; findDestr; reflexivity. 679 simpl; findDestr; reflexivity.
664 Qed. 680 Qed.
665 681
666 Hint Rewrite TBind_Answer : cpdt. 682 Hint Rewrite TBind_Answer : cpdt.
683
684 (** printing exists $\exists$ *)
667 685
668 Theorem tassociativity : forall A B C (m : thunk A) (f : A -> thunk B) (g : B -> thunk C), 686 Theorem tassociativity : forall A B C (m : thunk A) (f : A -> thunk B) (g : B -> thunk C),
669 thunk_eq (TBind (TBind m f) g) (TBind m (fun x => TBind (f x) g)). 687 thunk_eq (TBind (TBind m f) g) (TBind m (fun x => TBind (f x) g)).
670 intros; apply (thunk_eq_coind (fun m1 m2 => (exists m, 688 intros; apply (thunk_eq_coind (fun m1 m2 => (exists m,
671 m1 = TBind (TBind m f) g 689 m1 = TBind (TBind m f) g
834 | x :: ls' => Bind (f x) (fun x' => 852 | x :: ls' => Bind (f x) (fun x' =>
835 Bind (map f ls') (fun ls'' => 853 Bind (map f ls') (fun ls'' =>
836 Return (x' :: ls''))) 854 Return (x' :: ls'')))
837 end. 855 end.
838 856
857 (** remove printing exists *)
839 Theorem test_map : run (map (fun x => Return (S x)) (1 :: 2 :: 3 :: nil)) (2 :: 3 :: 4 :: nil). 858 Theorem test_map : run (map (fun x => Return (S x)) (1 :: 2 :: 3 :: nil)) (2 :: 3 :: 4 :: nil).
840 exists 1; reflexivity. 859 exists 1; reflexivity.
841 Qed. 860 Qed.