1

QF_NRA にゼロ除算は含まれますか?

SMT-LIB 標準は、この点で混乱を招きます。標準が定義されている論文では、この点について議論されていません。実際、NRA と QF_NRA はそのドキュメントのどこにも表示されていません。一部の情報は、標準 Web サイトで提供されています。実数は以下を含むものとして定義されます。

- 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.

これにより、定数値に関しては分母からゼロが明示的に除外されます。ただし、後で分割は次のように定義されます。

- / 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))t1t2

(/ m n)ゼロ以外の場合は実数にすぎないという記述にもかかわらず、ゼロによる除算が SMT-LIB に含まれているように見えるというのが事実上の現実nです。これは私の以前の質問に関連しています: y=1/x, x=0 は実数で満足できますか?

4

1 に答える 1

0

最初の引用は、(/ m 0) は数値ではないことを示しています

いいえ、しかし、それが何番であるかはわかりません。

しかし、後者の引用では、/ は (= t1 (/ t2 0)) が任意の t1 および t2 に対して充足可能であるような関数であると述べています。

正解です。

「0で割るな！」という学校のメンタリティから抜け出す必要があります。未定義です。未定義とは、これがどのような値であるかを指定する公理がないことを意味します。（これは学校でも同じです。）

とはf(1234)? これは定義されていないため、Z3 は任意の番号を選択できます。a / 0と の間に違いはありませんf(a)一部fの未解釈の関数です。Z3 は、好きな機能をすべて埋めることができます。

したがって、a / 0 == b満足でき、どれでもaOKbです。しかし(a / 0) == (a / 0) + 1、偽です。

算術演算子は単なる関数です。標準では、これらの機能を部分的に指定しています。

于 2016-10-21T20:05:58.870 に答える