潜水をしているような気分だ。

diary

潜水をしているような気分だ。深いところで何かを探っていて、ふっと海面から顔を出し、息をする。そしてまた深いところに潜り直す。

こういう気分になったのは修士課程以来だ。

何を探しているのかはわからないし、これがいい傾向なのかすらわからない。

pc

パソコンの調子が何かおかしい。

• メモリ: 問題なし
• SSD: 正常　
• HDD: 注意

おそらくこいつが悪さをしている。

雑に交換しよう。

今日の勉強

team

メモを一通り作れたので、summaryとして箇条書きを1つのファイルにまとめ、セクションを適当に区切った。

rust

TRPL pp.146-155

ベクタの中身を読む方法:

• 添字記法(&v[n])
  • &と[]を使って、
  • 参照を作る
• getメソッド(.get(n))
  • Option<&T>を取る
• 振る舞いの違い
  • ベクタに要素が含まれない番号の値を使用する
    • 添え字記法だと、パニックする
      • 存在しない要素を参照するから
      • ベクタの終端を超えて要素にアクセス使用としたときクラッシュさせたい場合に有用
    • getメソッドを使うと、Noneが返される
      • 普通の状態で、範囲外にアクセスする可能性がある場合に、有用
• 有効な参照がある場合、借用チェッカー(borrow checker)が所有権と借用規則を強要し、
  • ベクタの中身への、この参照や他の参照も有効であり続けさせる
    • 可変と不変な参照は同時に成立しない

1. ベクタがある。
2. ベクタのすでにある要素への参照を取る。
   1. 不変借用が発生する。
3. ベクタにpushする。
   1. 可変借用が発生する。
   2. ここで可変借用が発生するのは、ベクタが現在存在する位置に隣あっている要素を入れるだけの領域がない場合に、メモリの新規確保をして、古い要素を新しいスペースにコピーする、というベクタの動作法がある。
4. step2の参照を使おうとするとCompile Errorが発生する。

• ベクタの要素に順番にアクセスしたい。
  • forループで走査すればよい
    • ベクタの各要素に対して、
      • 不変な参照を得て出力したり
    • 可変なベクタであれば、
      • 可変な参照を走査して、参照外し演算子(*)を使用して、その値にたどり着き変更できる
• ベクタに異なる型の要素を保存させたい
  • ベクタは同じ型の値しか保持できない
  • enumを定義して、enum列挙子に異なる型の定義をし、enumの型のもとに定義されるようにすればいい
    • enumを使う利点
      • 各要素を格納するのに、ヒープ上でどれくらいメモリが必要になるかわかるように、
      • コンパイラがコンパイル時に入る型を知る必要がある。
    • enumを使う副次的利点
      • どんな型が許容されるのか明示できる
        • ただし、プログラマが保持される一連の型を知らない場合はenumのテクニックはうまくいかない
          • その場合は、TraitObjectを使おう

文字列

• 文字列で行き詰まる人が多い
  • 3つの概念の組み合わせで行き詰まる
    • Rustのありうるエラーを晒す性質
    • 文字列あ複雑なデータ構造であること
    • UTF-8
• 文字列をコレクションの文脈で語ることは有用である
  • なぜなら文字列は
    • テキストとして解釈されたときに有用になる機能を提供するメソッドと
    • バイトの塊で
    • 実装されているからだ
      • (メモ:これが理由となるのがわからない)
• 文字列
  • 言語の核としては１つの文字列型しかない
    • 文字列スライス
      • 別の場所に格納されたUTF-8エンコードされた文字列データへの参照
    • ライブラリ
      • 標準ライブラリのString
        • 伸長可能、可変、所有権のあるUTF-8エンコードされた文字列型
      • その他の色々な型があるが、その名前と性質は
        • XxxString: 所有権あり
        • YyyStr: 借用されたバージョン
  • 文字列式
    • String::new() -> String
    • String::from(文字列リテラル) -> String
    • 文字列リテラル.to_string
      • Displayトレイトを実装する型であればなんでもよい
      • 文字列はUTF-8エンコードされている
        • 適切にエンコードされていたらなんでもよい
    • s.push_str(文字列リテラル)
      • 文字列スライスを適用して、Stringを伸ばす
      • 所有権を得なくていいので、引数には文字列スライスを取る
• 文字列を組み合わせる
  • +演算子
    • let s = s1 + &s2
      • addメソッドを使っている
        • addメソッドのシグニチャはfn add(self, s:&str) -> String
      • s1の型はStringであり、この所有権を奪って、
      • 第二引数の中身のコピーを追記し、
        • s2の型はStringであり、addシグニチャの第二引数の型が&strで動くのか
        • コンパイラが型強制、参照外し型強制をしている
          • &sを&s[..]に変えていると考えてもよい
      • そして、結果の所有権を返している
  • format!マクロ
    • format!("{}...", s1, ...)
    • 可読性が高い
    • 引数の所有権を奪わない
    • Stringを返す

文字列に添え字でアクセスする

• 添え字記法でStringの一部にアクセスできない
  • Rustはそのサポートをしていないから
    • サポートしていない理由は、Rustがメモリにどのように文字列を保存しているかについての議論からわかる。

isabelle

Concrete Semantics

証明を追いかけたもの

• defs_restrict
• big_step_pres_approx_restrict
• approx_map_le
• restrict_map_le

疑問：declareの役割

declare assign_simp[simp]という表現がないと証明できない箇所があった。

declareの役割は何か？　useみたいな感じで引っ張ってきて、それにsimpで使うように宣言したりするようにすることか？

その線でやったら、declareしなくてもできたからこの認識で多少あっていそうだ。