PR
Keyword Search
▼キーワード検索
再生核研究所
再生核研究所声明
Calendar
Comments
Freepage List
2019.02.16
カテゴリ： カテゴリ未分類
ある種のソフトに ゼロ除算を採用しているは、凄いことで、ゼロ除算の 全く別な世界からの 導入として 高く評価されます。
奥村先生：
先ほどの方に メールしました。 Larry Paulson 氏の見解が、述べられていますが、 私の理解と同じで、彼らは、まだ真実を 知っていません。
下記の 文章です。
in 12 hours
José Manuel Rodríguez Caballero
Added an answer
I will reproduce here an email exchange with Prof. Lawrence Paulson (Cambridge) about the division by zero:
Extending the domain of division with x/0 = 0 (and also for integers) is a common choice in a great many systems, not just Isabelle/HOL but HOL Light, HOL4, MetiTarski and doubtless many other systems. They do it simply for convenience and not for any deep reason. The point is that many laws involving division will then hold unconditionally, an example being (a*b)/(c*d) = (a/c)*(b/d).
The technique of extending the domains of functions to simplify theorem proving goes back at least to the 1970s and the Boyer/Moore prover.
Larry Paulson
直接交流を図るようにしています。
ある種のソフトに ゼロ除算を採用しているは、凄いことで、ゼロ除算の 全く別な世界からの 導入として 高く評価されます。
敬具
齋藤三郎
２０１９．２．１６．１９：２０
2019年2月16日(土) 19:15
斎藤先生
これは強力な追い風でありますね。
奥村博拝
奥村先生：
先ほどの方に メールしました。 Larry Paulson 氏の見解が、述べられていますが、 私の理解と同じで、彼らは、まだ真実を 知っていません。
下記の 文章です。
in 12 hours
José Manuel Rodríguez Caballero
Added an answer
I will reproduce here an email exchange with Prof. Lawrence Paulson (Cambridge) about the division by zero:
Extending the domain of division with x/0 = 0 (and also for integers) is a common choice in a great many systems, not just Isabelle/HOL but HOL Light, HOL4, MetiTarski and doubtless many other systems. They do it simply for convenience and not for any deep reason. The point is that many laws involving division will then hold unconditionally, an example being (a*b)/(c*d) = (a/c)*(b/d).
The technique of extending the domains of functions to simplify theorem proving goes back at least to the 1970s and the Boyer/Moore prover.
Larry Paulson
直接交流を図るようにしています。
ある種のソフトに ゼロ除算を採用しているは、凄いことで、ゼロ除算の 全く別な世界からの 導入として 高く評価されます。
敬具
齋藤三郎
２０１９．２．１６．１９：２０
2019年2月16日(土) 19:15
斎藤先生
これは強力な追い風でありますね。
奥村博拝
お気に入りの記事を「いいね！」で応援しよう
Last updated
2019.02.16 19:23:40
【毎日開催】
15記事にいいね！で1ポイント
© Rakuten Group, Inc.
