Hi Conor and Peter,
Thanks a lot for the replies. They saved the day! While they exposed two
bugs for you, they also exposed one for me: another program which was
giving yellow marks (naive string matcher) was in fact not (provably)
total, so epigram rightfully gave me '?'. Which got me thinking how to
make it appear total. Options:
1. (easy) <= rec (append s os)
make the function recursive over the concatenation of the string and the
original string (which I have to pass around as there is no mutual
recursion). The length of these two together does decrease in all
recursive calls, so epigram should be happy. Unfortunately, <= rec
(append s os) won't work as far as I remember because the arg must be a
variable. Though some auxiliary functions might help. Will try.
2. accessibility predicates (Edwin's thesis) uhhh-uhhh. He says the
difficulty is in the termination proof, which I am inclined to believe,
and I haven't attempted it yet.
3. making the function structural (also Edwin's thesis). This looks
promising, I'll have a go at it later.
4. any other options?
I think I will have to read up on termination analysis! Thanks again for
the replies.
Laszlo
Conor McBride wrote:
Hi Laszlo
Laszlo Nemeth wrote:
Hi,
Could somebody please explain what to do about yellow question marks?
How can they arise in the first place? If I convinced the typechecker
that my program is total, what can go wrong? I'm trying to debug my
dead simple program(s): everything is green and yet all I get is '?'.
This usually means that the recursion-checker doesn't see why your
recursive call is ok. (Bug #1, the recursion checker should leave
suspicious calls with a yellow background, but it doesn't at the
moment; your program goes green after typechecking a dummy function
for the recursive call, then the machine tries to replace the dummy
with an appeal to an inductive hypothesis.)
------------------------------------------------------------------------------
( eq : all a : A => all b : A => Bool ; as, bs : List A !
let !--------------------------------------------------------!
! eqList eq as bs : Bool )
eqList eq as bs <= rec as
{ eqList eq as bs <= case as
{ eqList eq nil bs <= case bs
{ eqList eq nil nil => true
eqList eq nil (cons b bs) => false
}
eqList eq (cons a as) bs <= rec bs
{ eqList eq (cons a as) bs <= case bs
{ eqList eq (cons a as) nil => false
eqList eq (cons a as) (cons b bs)
=> eqListaux (eq a b) (eqList eq as bs) false
}
}
}
}
Am I making some stupid mistake? Why don't I get a value?
You're not making a stupid mistake, but you are unnecessarily
triggering the bug which is doing the real damage. Bug #2, if the
recursion checker is faced with a choice of inductive hypothesis, it
can sometimes commit too early to one possibility (I forget the
circumstances where this happens; it was a pretty hairy and hasty
hack.). Your <= rec bs is introducing such a choice, and it's
disappearing down this hole. I agree that it shouldn't, but that's
what happens just now.
The workaround is just to delete the <= rec bs node from your program.
In any case, it isn't needed: recursion on the first argument is
already enough. I just tried and it sorts out the problem.
Epigram 1's recursion checker was fairly rapidly thrown together from
not quite the right pieces. It was what I had lying around at the
time. Not too hard to send the thing the wrong way. Given how little
time I have available for hacking, I'm afraid I can't promise to fix
this bug. I can promise not to make the same bug in Epigram 2.
Many apologies
Conor
