2021-03-25

日記 2021/03/24, 2021/03/25

数学はすすんでない。

履修を見直した。

Factorioやったけど、厳しかった。

述語論理の形式モデルの実装は違う方法を思いついたので作っていたが、代入ですこしまた詰まった。

2021-03-23

日記 2021/03/23

$\langle \langle x, y \rangle, \langle x', f(x, y)\rangle \rangle$ の集合が実は関数 $h(x, y) = \langle x', f(x, y) \rangle$ であることが示せることが頭でわかった。証明はやってない。
述語論理の形式モデルの実装が進んだ。前述Variableの問題はホルダークラスを実装して回避した。
あと緑diffを2個解いた(Triangle と Rain Flows into Dams)。
ほかはなんもやってない。ボケ

2021-03-22

日記 2021/03/22

今日はほぼなんもやってない。

朝ちゃんと起きられたのはいいが、数学をほんの少し(自然数の掛け算に関する命題の証明やって、帰納定理の拡張

$\forall S (\forall a \in S; \forall f:N \times S \rightarrow N; \\\ \exists ! g : N \rightarrow S; ( g(0) = a \land \forall n \in N; g(n') = f(n, g(n)) ) )$

の証明で詰まってしまった(参考書にしている「数学の基礎」島内　に書いてある証明は最初に帰納的に関数を定義して、「これは関数だ」と言い切っているが、その証明には疑問がある)。

それでパソコンに逃げたら一日が終わった。

一応述語論理の形式モデルをC++で組もうとしたがこれも詰まった(項のクラス(class Term)から名前クラス(class Name)、変項クラス(class Variable)、引数を適用させた演算子クラス(class AppliedOperator)を派生させて仮想関数として項クラスに自由変項の集合を返す関数と、束縛変項を返す関数を実装しようとして、返り値をstd::unorderd_set<Variable>にしたら当然のごとく失敗した。

まず、Variableはユーザ定義クラスだからハッシュの関数オブジェクトを用意する必要がある。これは別に問題ないが、問題は基底クラスが派生クラスを含む型の戻り値の関数を仮想関数として宣言していることによる。

どうにか回避できないか試したが、そもそも構造に無理があるっぽいので他の方法を考える必要がある。

ちなみに、std::unordered_set<std::shared_ptr<Variable>>にするとコンパイルはできるが重複(ポインタの重複はしないが、ポインタの指す値の重複は起きる)するのでだめ。

形式さえできれば自然演繹でもシーケントでもして証明の妥当性判断ができそうで面白いはずなのでどうにかしたい。

また、証明の妥当性判断はそれはそれで面白そうだが、数学的対象をごちゃごちゃするのはそれだけだと不十分な気がしていて(例えば群の計算とかやる)、有限の場合は普通に実装できそうだけど無限の集合の扱いがどうすべきか。考えることはたくさんある(コンテナみたいに実装するんじゃなくて、対象と対象の関係を実装すればよさそう？)。