-
its_out_of_tune
- 3888
- 0
- 1
- 0
-
- いいね！0
ふみ (DJ Monad)
@fumieval
@myuon_myon 無論、意味論があってこその言語です。(理想的な)プログラミング言語は直観主義論理における命題の証明を記述する言語、というのは確かにそうですが、元々の議論における「数学」と同じように扱うのは違和感があります
2012-10-13 13:21:32
ふみ (DJ Monad)
@fumieval
「計算機のモデルが数学的に記述できる」ことと「プログラミングは数学を記述する言語である」ことは分けて考えているつもりです
2012-10-13 13:23:30
ふみ (DJ Monad)
@fumieval
@myuon_myon そうですね。「新たに定理を示す」と「定理を用いてものの性質を調べる」の二つがあると考えています
2012-10-13 13:25:14
ちゅーん
@its_out_of_tune
@fumieval 厳密には既に証明済みの論理なんでしょうけど、コーディングの過程でちょっとした（ライブラリだとかオブジェクトだとかの）「定理を示して」、そのものの「性質を調べる」っていう作業はプログラマが日常的にやってる気もするなぁ、とか。
2012-10-13 13:31:46
ふみ (DJ Monad)
@fumieval
@myuon_myon そもそも、私たちが実際に行っているプログラミングは、さっき述べたような理想的なプログラミング(定理の証明)と目的が異なるのではないか、と思っています
2012-10-13 13:32:44
ちゅーん
@its_out_of_tune
結局、数学とプログラミングを同一視して良いかどうかはわからんかったけど、ツイッターの議論で解るような事ならとっくに誰か証明しとりますかね。
2012-10-13 13:35:07
ふみ (DJ Monad)
@fumieval
@its_out_of_tune 「そのもの」を調べるのは定理を示すことに含められるのでは。「性質を調べる」は、何か数値を処理するのに解析学や線形代数を使う、などです
2012-10-13 13:36:58
ちゅーん
@its_out_of_tune
@fumieval ある集合の性質を調べるのに線形代数を使うのと、ある文字列の性質を調べるのに、Parseqを使う事がなんか根底にあるものは同じように見えるのは勘違いですかね(´・ω・｀)
2012-10-13 13:46:01
みょん
@myuon_myon
@fumieval 現実問題としては文さんの言っていることは正しいと思いますが、証明のためにプログラムを書く人や、予想だけして証明しない数学してる人だっていてもいいと思うんです それは今の話とは別の話なのかな、と
2012-10-13 13:48:05
ふみ (DJ Monad)
@fumieval
@its_out_of_tune なんとなく言いたいことはわかりました(linerlockさんのParseqが出てくるとは意外ですね)。性質を調べるために定理やライブラリを使うというのは普通のことですが、それによって得られた性質をどう使うか、というところに違いがあるのでは。
2012-10-13 13:50:26