> > line 9 : n1 is a legal value for passing it to 'fact', > > because n1 >= 0. Since n1 is a subset of n, the end > result > > is 1 (already computed), so f can only be a positive > > number. > > Do you have any ideas about the implementation of this, > specifically this: > > "the end result is 1 (already computed), so f can only be > a positive number." > > I have no idea how to implement this reasoning in a > computer program. The compiler has to prove that for every > call to fact the end result will be 1. So if you subtract > 1 from n you'll reach the base case eventually. > > Do you think it's possible to prove this in more complex > cases? To me this sounds like the halting problem...
Maybe a solution is to do it more like humans do, i.e. ignore the recursion, examine the code after the recursive point, extract the possible values from the operations, then go back and examine the recursive point with the new information at hand.
For example, one could say that:
1) after the recursive point, we have a multiplication. 2) we know 'n' is always positive in the recursive part. 3) we know the non-recursive path produces the value 1. 4) a multiplication of positive number to 1 produces another positive number. 5) the next step multiplies this positive number with N, which is another positive number. 6) therefore the result is a positive number.
Of course encoding the above in mathematical formulas may be impossible (I am only speculating here).
I think it's possible to prove it. If you can prove that the recursion will always hit the base case you're done. You can prove that n will get closer to the base case. That's pretty easy to prove. But if you evaluate fact(4.5) it won't stop. You don't have this problem in this case because the function only accepts integers, but there might be a similar problem with other functions (where the base case will be "skipped").
> I think it's possible to prove it. If you can prove that > the recursion will always hit the base case you're done. > You can prove that n will get closer to the base case. > That's pretty easy to prove. But if you evaluate fact(4.5) > it won't stop. You don't have this problem in this case > because the function only accepts integers, but there > might be a similar problem with other functions (where the > base case will be "skipped").
Let's say the integer constraint is relaxed and it is possible to do 'fact(4.5)'; Maybe it is not that difficult to prove 'infinite' recursion in this case, because the value '0' will never be produced by the subtraction n - 1. If the initial input is 4.5, then subsequent inputs will be 3.5, 2.5 ... 0.5, -0.5 etc.
Maybe algorithms can be classified into two categories: 1) those that recursion always hits the base case (as you've stated) 2) those that we can't prove recursion will always hit the base case. The presented approach might be useful for identifying and proving the correctness of computational problems of category 1, and also offer insights into category 2.
Anyway, I think that contracts can be equated with types, provided that it is possible to transfer all the assumptions we have in our brains to the computer.
lst should be nil for the process to stop, so cdr(x) should return nil for some value of x. If you apply cdr repeatedly: cdr(cdr(... lst ...)) it will produce nil (if you don't have circular lists).
It would be nice if the compiler can check this in the same way as fact(): with numbers. If you keep subtracting 1 from an integer n it will produce 0.
From this the compiler should be able to use the same reasoning as is needed for fact(). Of course, if fn loops forever, map will never return either...
; counts the leaves of a tree
; count-leaves('(2 3 (5 5) 4)) => 5
count-leaves(x:pair) = count-leaves(car(x)) + count-leaves(cdr(x))
count-leaves(nil) = 0
count-leaves(x:any) = 1
How can the compiler prove that this function is correct?
> From this the compiler should be able to use the same > reasoning as is needed for fact(). Of course, if fn loops > forever, map will never return either... > >
> ; counts the leaves of a tree
> ; count-leaves('(2 3 (5 5) 4)) => 5
>
> count-leaves(x:pair) = count-leaves(car(x)) +
> count-leaves(cdr(x))
> count-leaves(nil) = 0
> count-leaves(x:any) = 1
> > How can the compiler prove that this function is correct?
What exactly do we wish to prove for the count-leaves function?
From what I can see, there are no contracts for that function other than the types used.
cdr can only be called on a list, which has the contract of having a positive numer of elements or being empty, and makes the list shorter by 1 element. Provided that nothing is adding to that list (which it isn't here), you will eventually get to an empty list.
Returning to the "contracts == types?" question, the type for list provides this contract, and the programmer can expect that lists conforming to this contract (that is, cdr returns a list with one less item) will always work in this function.
If you were chasing pointers in the list, you could end up with a cyclic graph, which would make it possible to hit infinite recursion. However, the contract for a list says nothing about whether the items in that list refer to each other. You'd need another contract, and potentially another type. Say, a type that guarantees information about all objects of type X are kept in a hash map that can be used to tell if something's been visited. Like a Perl "inside out class."
Wait, unless you were wondering if the function would properly descend into lists inside that list. I keep studying Lisp, and I remember this is a problem, but I can't remember what the proper fix is.
Anyhow, if that's the case, then cdr doesn't provide the contract your lookig for. Or at least, it may not.
> Could you write the contracts for these functions? I'd > like to prove that the recursion will stop if you don't > have circular lists/trees.
First approach:
int count_leaves(l) {
ensure(l does not belong in set of values referenced by l);
if (l == null) return 0;
if (l is not a list) return 1;
return count_leaves(l) + count_leaves(next(l));
}
Obviously the above can not be proven stand-alone, but if put in context, then it might work. For example:
1 List l = new List;
2 append(l, l);
3 int c = count_leaves(l);
If we analyse the sets of values for the above code:
line 1: l = {nil} line 2: l = {l, nil} line 3: error; we see that the set of values of l contains itself.
Second approach:
Non-cyclic referencing could be proved by forbidding operations where the inserted element does not appear anywhere as the target list.
This second approach is similar to how humans operate: we form a collection of associations between variables, and then we search the code for list insertions where the inserted element does not appear in the collection of associations (at least that's what I do! :-)).
So, for example, if we have 3 lists A, B and C, and B was a member of A and C was a member of B, then we could see that it would be illegal to insert A into C, due to the following associations: A -> B -> C -> A.
Again, the issue here is how to represent the information/abstractions we have in our heads.
Flat View: This topic has 38 replies
on 3 pages
[
«
|
123
]
Previous Topic
