there_and_back_again.mlw 2.61 KB
 Jean-Christophe Filliatre committed Jun 12, 2013 1 `````` `````` Jean-Christophe Filliatre committed Jun 12, 2013 2 ``````(* Two puzzles from Danvy and Goldberg's ``There and back again'' `````` Jean-Christophe Filliatre committed Jun 12, 2013 3 `````` http://www.brics.dk/RS/02/12/BRICS-RS-02-12.pdf‎ `````` Jean-Christophe Filliatre committed Jun 12, 2013 4 ``````*) `````` Jean-Christophe Filliatre committed Jun 12, 2013 5 `````` `````` Jean-Christophe Filliatre committed Jun 12, 2013 6 7 8 9 10 11 ``````(* Computing a symbolic convolution: Given two lists [x1 , x2 , ..., xn−1 , xn ] and [y1 , y2 , ..., yn−1 , yn ], where n is not known in advance, write a function that constructs [(x1 , yn ), (x2 , yn−1 ), ..., (xn−1 , y2 ), (xn , y1 )] in n recursive calls and with no auxiliary list. `````` Jean-Christophe Filliatre committed Jun 12, 2013 12 13 ``````*) `````` Jean-Christophe Filliatre committed Jun 12, 2013 14 ``````module Convolution `````` Jean-Christophe Filliatre committed Jun 12, 2013 15 16 17 18 19 20 21 22 `````` use import int.Int use import list.List use import list.Length use import list.Append use import list.Reverse use import list.Combine `````` Jean-Christophe Filliatre committed Jun 12, 2013 23 `````` let rec convolution_rec (x y: list 'a) : (list ('a, 'a), list 'a) `````` Jean-Christophe Filliatre committed Jun 12, 2013 24 25 26 27 28 29 30 31 32 `````` variant { x } requires { length x <= length y } ensures { let (r, ys) = result in exists y0: list 'a. y = y0 ++ ys && length y0 = length x && r = combine x (reverse y0) } = match x with | Nil -> (Nil, y) | Cons x0 xs -> `````` Jean-Christophe Filliatre committed Jun 12, 2013 33 `````` match convolution_rec xs y with `````` Jean-Christophe Filliatre committed Jun 12, 2013 34 35 36 37 `````` | r, Cons y0 ys -> (Cons (x0, y0) r, ys) | _ -> absurd end end `````` Jean-Christophe Filliatre committed Jun 12, 2013 38 `````` let convolution (x y: list 'a) : list ('a, 'a) `````` Jean-Christophe Filliatre committed Jun 12, 2013 39 40 `````` requires { length x = length y } ensures { result = combine x (reverse y) } `````` Jean-Christophe Filliatre committed Jun 12, 2013 41 42 43 44 45 46 47 48 49 50 51 52 53 `````` = let r, _ = convolution_rec x y in r end (* Detecting a palindrome: Given a list of length n, where n is not known in advance, determine whether this list is a palindrome in ceil(n/2) recursive calls and with no auxiliary list. *) module Palindrome use import int.Int `````` Guillaume Melquiond committed Aug 21, 2014 54 `````` use import option.Option `````` Jean-Christophe Filliatre committed Jun 12, 2013 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 `````` use import list.List use import list.Length use import list.Append use import list.Nth use import list.NthLength use import list.NthLengthAppend predicate pal (x: list 'a) (n: int) = forall i: int. 0 <= i < n -> nth i x = nth (n - 1 - i) x exception Exit let rec palindrome_rec (x y: list 'a) : list 'a requires { length x >= length y } variant { x } ensures { exists x0: list 'a. length x0 = length y && x = x0 ++ result } ensures { pal x (length y) } raises { Exit -> exists i: int. 0 <= i < length y && nth i x <> nth (length y - 1 - i) x } = match x, y with | _, Nil -> x | Cons _ xs, Cons _ Nil -> xs | Cons x0 xs, Cons _ (Cons _ ys) -> match palindrome_rec xs ys with | Cons x1 xs -> assert { nth (length y - 1) x = Some x1 }; if x0 = x1 then xs else raise Exit | Nil -> absurd end | _ -> absurd end let palindrome (x: list 'a) : bool ensures { result=True <-> pal x (length x) } = try let _ = palindrome_rec x x in True with Exit -> False end `````` Jean-Christophe Filliatre committed Jun 12, 2013 93 94 `````` end``````