myuon_myon https://blog.hatena.ne.jp/myuon_myon/ Just $ A sandbox https://myuon-myon.hatenablog.com/ 定理証明 この記事はTheorem Prover Advent Calendar 2016 12日目の記事です。 この記事は定理証明初心者向けの記事です。 普段から依存型を用いた定理証明をされている方は読む必要がありません。 "coherence condition"と呼ばれる条件があり、訳すと「一貫性条件」となるようです。 これはちゃんと定義があるものではないのですが[要出典]、一貫性が保たれているならば当然成り立っているべき条件あるいは定理のことを、一般にcoherence conditionと呼んだりします。 例えば、型がついた言語での関数適用を考えます。 この時、P(Q,R)という項がwell-… 190 <iframe src="https://hatenablog-parts.com/embed?url=https%3A%2F%2Fmyuon-myon.hatenablog.com%2Fentry%2F2016%2F12%2F11%2F204537" title="依存型による定理証明Tips: coherenceは型で表せ - Just $ A sandbox" class="embed-card embed-blogcard" scrolling="no" frameborder="0" style="display: block; width: 100%; height: 190px; max-width: 500px; margin: 10px 0px;"></iframe> Hatena Blog https://hatena.blog 2016-12-11 20:45:37 rich https://myuon-myon.hatenablog.com/entry/2016/12/11/204537 1.0 100%