
From:  Fabio S. 
Subject:  Re: [Axiomdeveloper] Heidegger, literate programming, and communication 
Date:  Thu, 22 May 2014 19:25:13 +0200 (CEST) 
Useragent:  Alpine 2.10 (DEB 1266 20090714) 
...
And... the problem is be no means specific to AXIOM. foo(a: Integer, b: Integer): Integer == if a > 0 then if a > b then return foo(b,a) return foo(ba,a) return b Question: Does the program have a bug?I think that your question is related to the fact that if we don't know the purpose of a function then we cannot know if there is a bug in the function.And LP would explain the purpose of the function.
...My thought is that things are a little more complicated: you should explain both the purpose of the function and how it is implemented.
In this case, a little change in the "how" creates the problem: Ralf's function is clearly an implementation of the original (and inefficient) euclidean algorithm from the "Elements". Yet it gives wrong results, since he changed deliberately domain and codomain; for example, if a<0 then simply foo(a,b)=b.
The point is that the proof in the Elements assumes that a,b are PI.So to have a function without bugs either we need to change the domain to PIxPI or we need to add two auxiliary variables
c:=abs(a) d:=abs(b) and then we work with them.This is what I meant when talking about documenting maths: it can look correct from a syntactic point of view and can compile correctly, yet the result can be wrong. If the underlying math is advanced, the debugging is complicated by the fact that not a lot of people have the necessary knowledge to track the function and find the error: if it is not well documented, probably nobody will do it.
Just my 2 cents worth.
and these are just mine... Fabio
[Prev in Thread]  Current Thread  [Next in Thread] 