QF_NRA 中是否包含除以零? [英] Is division by zero included in QF_NRA?

问题描述

QF_NRA 中是否包含除以零?

Is division by zero included in QF_NRA?

SMT-LIB 标准在这方面令人困惑.定义标准的论文根本没有讨论这一点，事实上 NRA和 QF_NRA 没有出现在该文档的任何地方.标准网站上提供了一些信息.实数定义为包括:

The SMT-LIB standard is confusing in this matter. The paper where the standard is defined simply does not discuss this point, in fact NRA and QF_NRA do not appear anywhere in that document. Some information is provided on the standard website. Reals are defined as including:

- all terms of the form (/ m n) or (/ (- m) n) where 
  - m is a numeral other than 0,
  - n is a numeral other than 0 and 1,
  - as integers, m and n have no common factors besides 1.

当涉及到常量值时，这明确地从分母中排除了零.但是，后来，除法定义为:

This explicitly excludes zero from the denominator when it comes to constant values. However, later, division is defined as:

- / as a total function that coincides with the real division function 
  for all inputs x and y where y is non-zero,

接下来是一个注释:

Since in SMT-LIB logic all function symbols are interpreted as total
  functions, terms of the form (/ t 0) *are* meaningful in every 
  instance of Reals. However, the declaration imposes no constraints
  on their value. This means in particular that 
  - for every instance theory T and
  - for every closed terms t1 and t2 of sort Real, 
  there is a model of T that satisfies (= t1 (/ t2 0)). 

这看似矛盾，因为第一个引用说(/m 0)在QV_NRA中不是数字，而后一个引用说/是一个函数使得 (= t1 (/t2 0)) 对于任何 t1 和 t2 都是可满足的.

This is seemingly contradictory, because the first quote says that (/ m 0) is not a number in QV_NRA, but the latter quote says that / is a function such that (= t1 (/ t2 0)) is satisfiable for any t1 and t2.

实际情况是，被零除似乎包含在 SMT-LIB 中，尽管声明 (/mn) 只是一个实数，如果 n 非零.这与我之前的一个问题有关:y=1/x，x=0 在实数中可满足吗?

The de-facto reality on the ground is that division by zero seems to be included in SMT-LIB, despite the statement that (/ m n) is only a Real number if n is nonzero. This is related to a previous question of mine: y=1/x, x=0 satisfiable in the reals?

推荐答案

第一个引号表示 (/m 0) 不是数字

the first quote says that (/ m 0) is not a number

不，但它没有说明它是什么数字.

No, but it does not say what number it is.

但是后面的引用说/是一个函数，使得 (= t1 (/t2 0)) 对于任何 t1 和 t2 都是可满足的

but the latter quote says that / is a function such that (= t1 (/ t2 0)) is satisfiable for any t1 and t2

这是正确的.

您需要摆脱不允许除以零！"的学校心态.它是未定义的.未定义意味着没有公理指定这是什么值.(在学校也是如此.)

You need to get away from the school mentality that says "division by zero is not allowed!". It is undefined. Undefined means that there is no axiom that specifies what values this is. (And this is true in school as well.)

什么是f(1234)?它是未定义的，因此 Z3 可以选择任何数字.a/0 和 f(a) 之间没有区别，其中 f 是一些未解释的函数.Z3可以填任何它喜欢的功能.

What is f(1234)? It's undefined, so Z3 is allowed to pick any number at all. There is no difference between a / 0 and f(a) where f is some uninterpreted function. Z3 can fill in any function it likes.

因此，a/0 == b 是可满足的，任何 a 和 b 都可以.但是 (a/0) == (a/0) + 1 是假的.

Therefore, a / 0 == b is satisfiable and any a and b are OK. But (a / 0) == (a / 0) + 1 is false.

数学运算符只是函数.该标准部分规定了这些功能.

Mathematical operators are just functions. The standard partially specifies those functions.

这篇关于QF_NRA 中是否包含除以零?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！