3 ms·

This is a cool effort. Since agda : haskell :: coq : ocaml, I'm curious why agda wasn't used. Does it not not support extraction in the same way? I would lik

by chwahoo 16y ago

This is a cool effort. Since agda : haskell :: coq : ocaml, I'm curious why agda wasn't used. Does it not not support extraction in the same way? I would liked to have seen the talk itself since there are a few places in the slides where more detail would be nice. For example, I saw no reason why focusLeft on slide 40 wouldn't be total---it's not recursive, so why wouldn't it terminate? (given that reverse is total) I also wonder whether most functions in functional programs can be rewritten so that termination is evident due to structural recursion (like the transformation described on slide 41).

colanderman 16y ago
Never heard of Agda, thanks for the pointer. From what I read, it seems that Agda proofs are written declaratively, rather than interactively using tactics as in Coq. From experience, Coq's tactic-based proof system is very nice as it "unravels" the proof term in a way that makes it more manageable than balancing lambda terms in one's head. Regarding the question of totality on slide 40, a naïve analysis would say that the deconstruction "let (y : ys) =" could fail (if the list returned from reverse were empty), and thus the function would not be total. Of course this is not the case, since reversing a non-empty list returns a non-empty list, but this requires that reverse be dependently typed. (Slightly off-topic: the Mercury logic programming language supports just the right amount of dependency to allow this specification of reverse, and would deduce totality for this function.) Back on topic, yes, most practical functions can be rewritten to be structurally recursive. The most brain-dead easy way is add a "time-to-live" argument to the recursive function. This argument is a Peano number initially set to a value higher than the expected number of recurrences. (In the example from the slides, one could choose the total number of windows on the screen.) The function is then modified to decrement the time-to-live argument on each recurrence, and to return a dummy value should the time-to-live reach zero. It's then trivial to prove that the function terminates, and usually easy to prove that it does what it's supposed to do before the time-to-live zeros out.
- deleted 16y ago
  [deleted]
- chwahoo 16y ago
  > Regarding the question of totality on slide 40, a naïve analysis would say that the deconstruction "let (y : ys) =" could fail (if the list returned from reverse were empty), and thus the function would not be total. Of course this is not the case, since reversing a non-empty list returns a non-empty list, but this requires that reverse be dependently typed. You are right, I missed the deconstruction. Thanks!

by chwahoo 16y ago

colanderman 16y ago

Never heard of Agda, thanks for the pointer. From what I read, it seems that Agda proofs are written declaratively, rather than interactively using tactics as in Coq. From experience, Coq's tactic-based proof system is very nice as it "unravels" the proof term in a way that makes it more manageable than balancing lambda terms in one's head. Regarding the question of totality on slide 40, a naïve analysis would say that the deconstruction "let (y : ys) =" could fail (if the list returned from reverse were empty), and thus the function would not be total. Of course this is not the case, since reversing a non-empty list returns a non-empty list, but this requires that reverse be dependently typed. (Slightly off-topic: the Mercury logic programming language supports just the right amount of dependency to allow this specification of reverse, and would deduce totality for this function.) Back on topic, yes, most practical functions can be rewritten to be structurally recursive. The most brain-dead easy way is add a "time-to-live" argument to the recursive function. This argument is a Peano number initially set to a value higher than the expected number of recurrences. (In the example from the slides, one could choose the total number of windows on the screen.) The function is then modified to decrement the time-to-live argument on each recurrence, and to return a dummy value should the time-to-live reach zero. It's then trivial to prove that the function terminates, and usually easy to prove that it does what it's supposed to do before the time-to-live zeros out.

deleted 16y ago
[deleted]
chwahoo 16y ago
> Regarding the question of totality on slide 40, a naïve analysis would say that the deconstruction "let (y : ys) =" could fail (if the list returned from reverse were empty), and thus the function would not be total. Of course this is not the case, since reversing a non-empty list returns a non-empty list, but this requires that reverse be dependently typed. You are right, I missed the deconstruction. Thanks!