なのログ

だから見てて下さい・・・俺の・・・変身

型システム入門を読んでいます(第8回)

またお久しぶりになってしまいました。型システム入門です。
今確認したら1ヶ月以上空いてますね。うわあ。これは罪では。
今回でやっと5章2節「ラムダ計算でのプログラミング」を抜けます。

これまでのあらすじ!

「ラムダ式いうのがあるんか」
「こうやってやるんやな」
「うわすっご・・・」
「うわすっご・・・」
「うわすっご・・・」

だいたいこんなんッスね(語弊)
ラムダ式のいろんな計算例を見ました」ということを言いたい模様。

ではやっていきましょう。


計算体系の拡張

「3章で定義したやつ、組み込んだろか」の意。

これは物議を醸す。
3章で定義したやつというのは、このへんのことです。

bool値
    t ::= 
        true                <- 真
        false               <- 偽
        if t then t else t  <- 条件式
    v  ::= 略!

数値
    t ::=
        0
        * t              <- 後者値
        pred t              <- 前者値
        iszero t            <- ゼロ判定
    v ::= 略!
    nv ::= 略!

「それマジで言ってる・・・?喧嘩しない・・・?」

真偽値 tru <-> true

    realbool = λb. b true false
    realbool tru
    ->  (λtf. t) true false
    ->  true

    churchbool = λb. if b then tru else fls
    ->  churchbool true
    ->  if true then tru else fls
    ->  tru

なんとなく理解。「ラムダの識別子なんでも入るし確かにな?」という感想。

数値 Church数 -> プリミティブ値

    realnat = λm. m (λx. succ x) 0
    realnat C3
    ->  C3 (λx. succ x) 0
    ->  (λsz. s ( s ( s z))) (succ 0)
    ->  (succ (succ (succ 0)))
    ->  3

これは逆にはできないっぽいですね。
プリミティブ値というか算用数字というか、逆のほうは構造的な意味がないので仕方なさそう。
for文みたいのが定義されていればよかったんでしょうが、それはまあ違う話と言えそう。

再帰

「発散コンビネータ」なるものがあるようです。

    omega = (λx. x x) (λx. x x)

名前カッコええな・・・。
この式ですが、簡約を続けても同じ形のままです。

そしてその一般化(?)があるらしい。ここの流れはよくわからんのですが。

    fix = λf.(λx. f (λy.x x y)) (λx. f (λy.x x y))
    (なんでxとかyとか増えたんだろう・・・)

Yコンビネータとか不動点コンビネータとかいうやつみたいです。

メッチャこのへんで見た。
(2017年10月のアレ)

で、再帰です。fixで遊べる様子。
であれば階乗関数factorialを作ろうという試みに。

階乗でやりたいことを書きます。(書中だと式が表現しています)

数Nを階乗()に入れて 階乗(N)をするかんじで。
    階乗(N)
    ->  Nが0のとき1を返す
    ->  Nが1以上のときそのN*階乗(N-1)

F#で表現すると。(!?)

    let rec factorial n = function
        | 0 -> 1
        | n -> n * (factorial (n-1))

はい。これを見た型システム入門の読者は次のように思わなければなりません。そんなことはない。

まず g = λf.(fを含む本体)と定義し、次に h = fix g と定義する。    

となるとこう定義するようです。

    g = λfct. λn. if realeq n C0 then C1 else (times n (fct (prd n)))
    factorial = fix g

???????

困る。

せ、整理をしてみましょう。

    g = λfct.
        λn. if realeq n C0    // ゼロ判定
            then C1    // ゼロのとき1
            else (times n (fct (prd n)))    // それ以外もさっきのF#とかの表現のまま

    factorial = fix g

インデント入れたらわりとまんまだコレ!

思いのほか整いました。すごい。


というかんじで今回はこんなもんです。世界拡張回。
で、閉じたところでなんですが、さっきのfactorial、「fixの意味は・・・?」という気持ちが湧いてしまいました。
ちょろっと考えましたがわかりません。また時間のあるときに式を試しにこねてみます。

というのもですね、実は今回の更新、1月に1記事もなくなる事態を危惧しての駆け込み回でした。
正月期間とか二週間くらい前とかに多少書きつつ、ずっと下書き保存状態でした。
わりと反省の色が濃い感がありますが、なんだかんだで読み進めると楽しんでいるので、2019年も読み進めていきたいところです。スーパー牛歩。

ではまた!