プログラミング言語の基礎概念

https://gyazo.com/1c9d8e37c245e95aa1361c2eb5854ba8

とりあえず以下のように記述される

0⇛Z

1⇛S(Z)

2⇛S(S(Z))

Zはゼロのこと

Sは後継者、次に転じるものの意

自然数の導出システムとしてNatを導入する

plusなのかtimesなのか

加算と乗算ができるもの

推論規則(加算)

P-ZERO：　任意のペアノ自然数nに対して判断 Z plus n is nを導いてもよい

（任意の自然数nについて）0とnの和はnである

P-Succ: 任意のペアノ自然数n1,n2,n3に対してn1 plus n2 is n3 ならば　S(n1) plus n2 is S(n3)を導いてもよい

任意の自然数n1,n2,n3についてn1とn2の和がn3ならばn1の次の数とn2 の和は(n3の次の数)である

乗算

T-ZERO：Z times n is Z

T-SUCC: n1 times n2 is n3 かつ　n2 plus n3 is n4 ならば S(n1) times n2 is n4

導出自体は分かったが順番ステップが分かっていないかも

つまり

一番下に 証明したい式を書いて

使える規則を使って左の引数がZまでやる

規則を使う時に代入するというよりはパターンマッチして剥がすみたいな間隔でおこなう

Zになったらおわりって感じね

括弧をなるべき省略する

計算途中におこなってもよい

矢印で示す

定理の定理みたいなこと

この章は最初に読む人限定で読み飛ばしてもいいらしい

戻ってくるかも

×と＋では×の方が結合が強い

括弧の意味についても定義しなければならない

エラーについてもどうように定義する

条件分岐のエラーの時

if e1 then e2 else e3

みたいなときにe1の値によってe2かe3のどちらか一方を評価する

e1の値が仮に真偽値出ない場合はどちらも評価せずにエラーにする

trueの場合はelseは評価しない

当たり前だけど変数は名前の宣言、宣言された変数を参照、空間的・時間的に有効なスコープが要件としてある

関数と再帰

◯ * ◯や if ◯ < △ then △ else ◯

みたいに◯や△などの穴のあいた式である

計算のパターンを抽象化したものが関数

結果を返り値

関数に関する関数

関数を引数とする関数

クロージャのこと

式を評価した時点での値が必要になる

関数の式に関する情報とパラメータ以外の変数の値を組にしたもの

静的有効範囲と名前なし表現

変数というのは環境（スコープ）が判断毎に異なるにもかかわらず出現に対しては一定、

束縛が環境の何番目にあるかは式を見ればわかる

今までの導出システムの作る流れを見てきたからかも

名前を使わずに引数（束縛変数）を参照するための記法

リストの基本的な操作は以下2つ

どのように構成されているか

空なのか調べる

リストを分割する操作

パターンマッチング

複合的なパターンの抽出に加えて網羅的ではないものと重なりのあるパターンも検知できる

ある環境の中で与えた型以外の値が設定された場合はその式は評価しない

エラーになることも定義する

多相（polymorphism）多くのという意味のpolyと形態を示すmorphからきている

様々な形態を持つという意味

定義、式、操作が様々な異なる文脈で使用できることを意味する

いくつかの多相性がある

型の中身を一切見ない、どんな型でも同じように動くこと？

ひとつの式が持つ複数の方のパターンがパラメータを使って統一的に表せる

型ごとに違う実装を選ぶ。同じ名前の関数が、型によって別の動きをする。

オーバーローディング

一つの式に複数の型が与えられるもの、それらの型に特に一定のパターンがない（場当たり的）

型 S が型 T の部分型なら、T が期待される場所に S を渡せる

まだ具体的に決まっていない型

型スキームは型変数を全称量化（∀, forall） で明示的に束縛したものかな

型推論のアイデアとして方程式がある

新たに宣言された変数の型がわからない場合はひとまず方変数で表してその型変数に関数る方程式をたてるといい

2つの項（式）SとTに対し、あるα置換を適用して両者を同一の項に導く処理