我正在TeX中编写一个(几乎)IEEE 854兼容的浮点实现(它只支持32位整数).该标准仅规定的结果+,-,*,/,比较,余数,并且sqrt:对于这些操作,结果应(根据舍入模式)是相同的舍入准确结果的表示的数.
我似乎记得IEEE指定超越函数(sin,exp...)应该产生忠实的结果(在默认的舍入到最近的模式中,它们应该输出围绕确切结果的两个可表示数字之一).计算小数的正弦是相当简单的:移动2*pi的倍数以获得[0,2*pi]范围内的数字,然后再做一些工作以将范围缩小到[0,pi/4] ,并使用泰勒系列.
现在假设我想计算sin(1e300).为此,我需要找到1e300 modulo 2*pi.这需要知道pi的300(316？)个小数,因为只有16个小数,结果没有任何意义(特别是,它不是忠实的).
关于结果sin(1e300)和类似的非常大的数字应该有标准吗？
其他浮点实现有什么作用？
我读了一些if a then b else c代表的教程match a with true => b | false => c end.然而前者非常奇怪地没有检查类型a,而后者当然确保它a是一个布尔值.例如,
Coq < Check if nil then 1 else 2.
if nil then 1 else 2
: nat
where
?A : [ |- Type]
Coq < Check match nil with true => 1 | false => 2 end.
Toplevel input, characters 33-38:
> Check match nil with true => 1 | false => 2 end.
> ^^^^^ …