[EMAIL PROTECTED]:/work/felix/svn/felix/felix/trunk$ f
test/regress/rt-1.01.54-0.flx
Assertion2 Failure
Felix location: ./lpsrc/flx_regress.pak 2232[1]-2232[26]
C++ location : test/regress/rt-1.01.54-0.cpp 81
Felix location: lib/flx_tclass.flxh 70[3]-70[3]
C++ location : test/regress/rt-1.01.54-0.cpp 81
{if(FLX_UNLIKELY(!(- 0.1 * (0.4 + 0.7 ) == - 0.1 * 0.4 + - 0.1
* 0.7 )))
axiom distrib (x:t,y:t,z:t): x * ( y + z) == x * y + x * z;
Well .. of course the distributive law doesn't hold for
floats. The question is .. what to do about it?
Options:
1. Change 'eq' for floats
2. Change the axiom for floats to be
axiom distrib (x:t,y:t,z:t): close (x * ( y + z), x * y + x * z);
where close (a,b) provides some norm on floats, eg:
fun close (x:float,y:float)=> abs(x,y) < 0.001;
This is numerically unsound, but it is good enough for
testing axioms.
The problem may be that this makes it impossible to
use the law logically, eg in proofs etc. Although perhaps
this is indeed right.
--
John Skaller <skaller at users dot sf dot net>
Felix, successor to C++: http://felix.sf.net
-------------------------------------------------------------------------
Using Tomcat but need to do more? Need to support web services, security?
Get stuff done quickly with pre-integrated technology to make your job easier
Download IBM WebSphere Application Server v.1.0.1 based on Apache Geronimo
http://sel.as-us.falkag.net/sel?cmd=lnk&kid=120709&bid=263057&dat=121642
_______________________________________________
Felix-language mailing list
Felix-language@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/felix-language
