rb@ccird1.UUCP (06/20/86)
In article <1245@lsuc.UUCP> dave@lsuc.UUCP (David Sherman) writes: >In article <269@ubc-cs.UUCP> andrews@ubc-cs.UUCP (Jamie Andrews) writes: >> It should be of little concern to applications programmers that >>these features destroy the declarative reading of the program, unless they >>have to prove to their bosses that their applications are rigorously >>correct. > >Interesting issue. What happens if I succeed in designing a tool >which can be used for corporate tax planning, and I want to make >it a commercial product? Should it be "provably" correct before >lawyers use it? I've been following your progress with this package, and you should be commended for what your doing. I am working on a "software analysis" package which is similarly complex. There are different degrees of "provably correctness" of any program in any language. Fortunately, prolog makes it very easy to verify the correctness. In effect, the issue here is when to "bind" a fact that depends on other facts. If one declares that "child(a,b). child(b,c). child(b,d)" then for some reason new facts implicitly or explicitly change those facts so that additional cases are true, the bindings of "related(a,X)" (related meaning all the children, grandchildren...) would be changed as well. The issue of dynamic binding is not new. Theoretically, to be "provably correct" only the absolute facts should ever be bound, but for practical reasons, this is rarely the case. The process of reproving a theorum in which the axioms are rarely changed can be quite costly. The point here is that it is necessary to know when the axioms have been changed, a mechanism that prolog seems to lack. When using assert, you are effectively saying that these rules are valid for "the current set of facts". Using your "controls" example, if someone makes the transition from "not controls" to "controls" after you have made your assertions, and inductions have been made before the reassertions have been made, then the solution is provably wrong. Suppose your algorythm for "controls" depends on purchases of stock, suppose also that there are certain tax benifits or penalties that go into effect at the time the person takes control. You might retract/assert at the end of each day, but between the time someone took control, and the time you re-asserted, the man made 2 million in capital gains profits. Or conversely he make the money at 10:00 AM, and takes control at 1:00 PM. Again you've missed the benefits/penalties. If the rules are set to the hour, retract/asserts could be done hourly, if they are by the day, they could be done by the day. In fact, although the law might not be "provably correct", if the law specified that benifits go into effect the day that a person takes control, then you MUST retract/assert before you do any benefit calculations. A good example of this would be the guy who got married on December 31. In this case, the filing status, benifits, and penalties would be the same as if he had been married on January 1, however the witholding status would not have changed until the following year. To flatly say that assert/retract is a no-no, or is incorrect is incorrect. Uses of assert/retract should reflect the rules or laws being represented. To answer your question, yes it should be "legally correct" rather than "mathmatically correct" before lawyers use it. This may mean that you MUST use retract/assert. The law is not always logical. This may also mean that rules must be put into separate files, based on their granularity, so that audits can be performed. This brings up the need for a new feature of prolog. Namely, the ability to "save" only a particular set of rules to a specific, named file.
dave@lsuc.UUCP (David Sherman) (07/07/86)
In article <506@ccird1.UUCP> rb@ccird1.UUCP (Rex Ballard) writes: >The issue of dynamic binding is not new. Theoretically, to be "provably >correct" only the absolute facts should ever be bound, but for practical >reasons, this is rarely the case. The process of reproving a theorem >in which the axioms are rarely changed can be quite costly. > >The point here is that it is necessary to know when the axioms have been >changed, a mechanism that prolog seems to lack. When using assert, you >are effectively saying that these rules are valid for "the current set >of facts". What I'm planning to do is use something like Kowalski's "holds" formulism, to state that something either stated or derived as true at a given time is still true at a later time unless we know otherwise, and have a number (from zero up) of ways for each predicate to possibly become untrue. For example, an assertion about sharesoutstanding(Corp, Class, Numshares) can become untrue in at least three ways: if new shares are issued; if shares are redeemed; and if the corporation is wound up. >Using your "controls" example, if someone makes the transition from >"not controls" to "controls" after you have made your assertions, >and inductions have been made before the reassertions have been made, >then the solution is provably wrong. Suppose your algorithm for >"controls" depends on purchases of stock, suppose also that there >are certain tax benefits or penalties that go into effect at the >time the person takes control. You might retract/assert at the >end of each day, but between the time someone took control, and >the time you re-asserted, the man made 2 million in capital gains >profits. Or conversely he make the money at 10:00 AM, and takes >control at 1:00 PM. Again you've missed the benefits/penalties. I should point out that I'm not designing a "real-time" system here which will chug along each day and tell you what the current state of the world is. My system will be an analysis tool, which can be used either to review past facts or to consider proposed facts. So the granularity of the events which are relevant is determined by the person specifying the facts, and of course the program has to adjust its conception of what is true at each point in time at which anything happens. >To answer your question, yes it should be "legally correct" rather >than "mathematically correct" before lawyers use it. This may mean >that you MUST use retract/assert. The law is not always logical. Canadian income tax law is highly logical, which is why I'm using Prolog. I think I may need to use retract/assert, but I don't think the reason is that the law is not logical. Dave Sherman The Law Society of Upper Canada Toronto -- { ihnp4!utzoo pesnta utcs hcr decvax!utcsri } !lsuc!dave