読者です 読者をやめる 読者になる 読者になる

あのねノート

せんせいあのね、パソコンで字が書けるようになったよ

勉強してました

とりあえず今日の勉強時間は終わってゆっくり寝る態勢に入っていこうということで今日のことを書きます。

今日はずっとデータベースの多値従属性というので悩んでいました。
多値従属性 - Wikipedia
属性A,B,Cがあるときに、AとCが決まったとき対応するBの値があるけど、BはAだけに依存しててCからは独立してるってことだそうです。正直これならC要らなくね?と思いました。
例を読んだら意味は分かるんだけど自分の作るデータベースに無理やりその要素を入れないといけないところが難しかったです。そもそも多値従属性があったら正規化してしまうものだし、多値従属性が入った表なんて冗長なんだから最初から表を分けて回避するんじゃないのかと思ってしまいました。6時間溶かして従属性作ったけどレポート書くのめんどくさくなったしすでに6時間も使っちゃってるし、従属性のあるER図を作ったところで放り投げてしまった。まあすぐ書けるでしょう…信じてる…

残り2時間だなということで昨日もやったCoqの予習の続きをしました。なんで授業はスライドなのにわたしはあとからスライドの手書きまとめノートを作ってて手書きプログラミングしてるんだろうと思いました。しかも手書きしてやっとこさ理解できるあたりが自分の才能のなさを感じさせます。まあそういうこともありますね。

Inductive day : Type :=
  | monday : day
  | tuesday : day
  | wednesday : day
  | thursday : day
  | friday : day
  | saturday : day
  | sunday : day.

でいちいち「mondayはday型!tuesdayもday型!」って言うのなんでだろうって話になって考えてたのですが、そのあと

Inductive nat : Type :=
  | O : nat
  | S : nat -> nat.

こういうのが出てきて、「でもSはnat型を受け取ってnat型にするコンストラクタ!」って言ってるんだなと気づいたのが発見でした。友達と一緒に勉強すると賢くなるスピード速そう。
あとコンストラクタと関数の違いについて

These are all things that can be applied to a number to yield a number. However, there is a fundamental difference between the first one and the other two: functions like pred and minustwo come with computation rules — e.g., the definition of pred says that pred 2 can be simplified to 1 — while the definition of S has no such behavior attached. Although it is like a function in the sense that it can be applied to an argument, it does not do anything at all! It is just a way of writing down numbers.

とあったのは「関数は計算してるけどコンストラクタは元の値にくっついてるだけ」と思えばいいのかな。
例に

(Think about standard arabic numerals: the numeral 1 is not a computation; it's a piece of data. When we write 111 to mean the number one hundred and eleven, we are using 1, three times, to write down a concrete representation of a number.)

とあったのでコンストラクタは111と一緒でデータに何かくっついてできたデータ(この場合は数字)を表してるだけでデータで計算してるわけじゃないってことかなあと思ったのですが…
111は1を使って何か計算してるんじゃなくて111という数字そのものを表してるだけなのと同じように、(S O)はOを使って計算してるんじゃなくてOにSがくっつくことで表せる数字そのものを表してるのであってこれ以上書き換えできない、みたいな…日本語が下手だ。111がこれ以上書き換えられないのと同じようにコンストラクタのついた(S O)も書き換えられないけど、関数を使ったplus (S O) (S (S O))は(S (S (S O)))に書き換えられるよねってことかなと思ったのですが…この辺詳しくないのでよくわかんない。そんな厳密な理解がなくてもここは切り抜けられるけど後で必要になったら困るなあなどと考えていました。弱者なので誰か教えてくださいという感じ。

これから授業についていけるだろうか、がんばりたいです。(あとCoqの式書くのにOcaml書いてることにしたんですけどこれで大丈夫なんだろうか)