今日の記録 2020/6/12
仕事
インスタグラムの埋め込み
美容師などを中心に、Webページへのインスタの埋め込みの需要が結構あるようなのだが、現在の API の仕様だとインスタのアカウントを持っている人にいろいろやってもらう必要があってかなり面倒なことになっていた。少し調べた限りでは途中で嫌になるレベルでの作業量だったので、顧客にスムーズにやってもらうには分かりやすい資料等を作る必要がありそうだった。こちら側でできる部分と、アカウントの所有者でしかできない部分を分けてまとめる必要がある。
デザインの設計方法
ブラウザ上で css や html を書きながらデザインを考えることを Designing in Browser というらしい。レスポンシブデザインをするためには様々な画面サイズでの設計をする必要があり、すべてについてデザイン案を作るのはとても手間である、という理由でこのデザイン方法が使われるそうだ。何も知らずにこの方法でデザインを考えていたのだが、正直自分には全く合っていないと感じている。デザインとコーディングは分けてやった方がひとつの問題に集中できそうだと感じているので、別な手段というか別々にやるフローのようなものを調べてやりたい。
勉強した
GEB - 206
証明と導出の違いに関する話題があるのだが、この本では、証明というのは人が言葉を使って非形式的に何かを結論付けたりするもので、導出というのが（今回の論理計算のような形式システムを用いて）形式的にある目的に到達するものとして書かれている。直感的には、証明に対しても形式的であるようなイメージを持つ。これは単に、いままでは導出というべきところでも証明という言葉を使っていたために起こっている混乱であって、もともと論理的な導出を証明と言うのが変だった、ということになるのだろうか。それともこの証明と導出という言葉の使い分けというのはこの本の中での話であって、この二つに明確な使い分けの基準が無いという可能性もあるだろうか。
「What's the difference between a proof and a derivation? 」という質問の StackExchange の投稿への解答のひとつとして以下の答があった。
「Mathematically, Proof is any derivation that validates a Theorem. And Derivation is a mathematical procedure which is performed on the basis of axioms and other known theorems.」
この文章からは、数学的にはという前提の元で、証明というものが導出という動作を利用して何か定理を検証するためのもので、導出というのは既知の公理や他の定理を用いて行われる数学的な手続きである、というものだった。つまり、この文章が正しいとすれば、証明という行い自体が導出という形式的な行いを含んでいると考えられそうだと思える。
だが以下の別な解答では話が違っており、どちらかと言えば GEB の本文内での意味に近いものになっている。どちらにもこれといった根拠はないので、「導出」という単語を当ててよいケースより、「証明」という単語を使うことができる範囲はより広い、というような結論にするしかないだろうか。
But it's not a proof that most mathematicians will consider "a proof", as "proving something" in mathematics is more of an abstract derivation, than verifying an instance of the proof.
閑話。「命題の論証の進め方をきれいな形式システムによって研究することは、純粋数学の魅力的な分野のひとつである。」という一文がある。プログラミングにおいては、型システムというものが形式システムの中でも身近なものの一つであり、プログラミングをしていると型システムそのものへ興味が湧く。型システム、および論理学への興味から、学生時代に『ソフトウェアの基礎』という本を読んでいたのだが、これも途中で読むのを(いつのまにか)やめていた本のひとつだ。これも今後の並行読書のリストに加えてまた再挑戦したい。前は Emacs の Proof General というものを利用して Coq を動かしていたが、今だと VS code あたりにいい感じのものができていたりしないだろうか。
この記事が気に入ったらサポートをしてみませんか？