variable x ok 3 ok 1 x ok 2 ! ok ( これで、x に 3 が代入される ) ok x ok 1 ( スタックに入れた段階では、 x がスタックに入っている ) @ ok 1 ( @ をかますと、x の皮がむけて、3 が出現する ) スタック <1> 3
5 ok 1 x ok 2 + ok 1 ( 5 x + をやると、変な答えになった ) スタック <1> <x+$5>
Forth をやってみた
Forth は、スタック指向のプログラミング言語だ。
ここの記事が参考になった。
Forth でコラッツ
:~/me/Forth$ cd collatz :~/me/Forth/collatz$ gforth Gforth 0.7.9_20201105 s" collatz.f" included ok 5 ok 1 collatz ok 6 .s <6> 5 16 8 4 2 1 ok 6 . . . . . . 1 2 4 8 16 5 ok 27 ok 1 collatz ok 112 dangerAllOut 1 2 4 8 16 5 10 20 40 80 160 53 106 35 70 23 46 92 184 61 122 244 488 976 325 650 1300 433 866 1732 577 1154 2308 4616 9232 3077 6154 2051 4102 1367 2734 911 1822 3644 7288 2429 4858 1619 3238 1079 2158 719 1438 479 958 319 638 1276 425 850 283 566 1132 377 754 251 502 167 334 668 1336 445 890 1780 593 1186 395 790 263 526 175 350 700 233 466 155 310 103 206 412 137 274 91 182 364 121 242 484 161 322 107 214 71 142 47 94 31 62 124 41 82 27 *the terminal*:8:1: error: Stack underflow >>>dangerAllOut<<< Backtrace:
自然数の加法の交換法則 by Idris
これは「Idris Advent Calendar 2020 - Qiita」の6日目の記事です。
Idris で自然数の加法の交換法則を証明してみましょう。
以下のように Comm.idr を書いて、ロードします。
関数commの型だけを書いた状態です。
%default totalはおまじないだと思ってください。
module Comm %default total comm : (x, y : Nat) -> x + y = y + x
$ idris ...... Idris is free software with ABSOLUTELY NO WARRANTY. For details type :warranty. Idris> :l Comm Type checking ./Comm.idr Holes: Comm.comm *Comm> :t comm x : Nat y : Nat -------------------------------------- comm : plus x y = plus y x Holes: Comm.comm *Comm>
:l Commでモジュールをロードしています。
:t commで関数commの型を確認しています。
これで型定義が確認できました。
自然数の定理の証明方法として、
引数の自然数をZ(0)とS(+1)に分ける、という方法があります。
今回は引数が2つあるので、4パターンに分けられます。やってみましょう。
comm : (x, y : Nat) -> x + y = y + x comm Z Z = ?rhs1 comm (S x) Z = ?rhs2 comm Z (S y) = ?rhs3 comm (S x) (S y) = ?rhs4
*Comm> :l Comm Type checking ./Comm.idr Holes: Comm.rhs4, Comm.rhs3, Comm.rhs2, Comm.rhs1 *Comm> :t rhs1 -------------------------------------- rhs1 : 0 = 0 Holes: Comm.rhs4, Comm.rhs3, Comm.rhs2, Comm.rhs1 *Comm>
?rhs1というのは Hole です。?の後の文字列は何でも良いです。
Idris では、分からない部分は Hole にしておいて、とりあえずロードする事ができます。
Hole を:tすると、その部分の型を示してくれます。
(Z, Z)の場合
フライングで出ちゃってますが、Hole rhs1 の型は0 = 0でした。
両辺の値が等しい時は、Reflが使えます。
comm : (x, y : Nat) -> x + y = y + x comm Z Z = Refl comm (S x) Z = ?rhs2 comm Z (S y) = ?rhs3 comm (S x) (S y) = ?rhs4
*Comm> :l Comm Type checking ./Comm.idr Holes: Comm.rhs4, Comm.rhs3, Comm.rhs2 *Comm>
Hole が一つ減りましたね。
(S x, Z)の場合
*Comm> :t rhs2 x : Nat -------------------------------------- rhs2 : S (plus x 0) = S x Holes: Comm.rhs4, Comm.rhs3, Comm.rhs2 *Comm>
Hole rhs2 の型はこのようになっています。
x + 0 = x ですから、この部分を計算したいですね。
標準ライブラリを探すと、plusZeroRightNeutralという関数があるので、これを使います。
また、「rewrite」という構文を使います。
ある式に対して、等式を持ってきて、ある式の中で左辺に該当する部分を右辺に置き換えます。
エディタで置換するようなものです。
comm : (x, y : Nat) -> x + y = y + x comm Z Z = Refl comm (S x) Z = rewrite plusZeroRightNeutral x in ?rhs2 comm Z (S y) = ?rhs3 comm (S x) (S y) = ?rhs4
*Comm> :l Comm Type checking ./Comm.idr Holes: Comm.rhs4, Comm.rhs3, Comm.rhs2 *Comm> :t rhs2 x : Nat _rewrite_rule : plus x 0 = x -------------------------------------- rhs2 : S x = S x Holes: Comm.rhs4, Comm.rhs3, Comm.rhs2 *Comm>
おおお、左辺と右辺が一致しましたね。これでReflが使えます。
(Z, S y)の場合
この場合もさっきとほぼ同じなので、同様に処理します。
comm : (x, y : Nat) -> x + y = y + x comm Z Z = Refl comm (S x) Z = rewrite plusZeroRightNeutral x in Refl comm Z (S y) = rewrite plusZeroRightNeutral y in Refl comm (S x) (S y) = ?rhs4
*Comm> :l Comm Type checking ./Comm.idr Holes: Comm.rhs4 *Comm>
Hole は残り一つです。
(S x, S y)の場合
*Comm> :t rhs4 x : Nat y : Nat -------------------------------------- rhs4 : S (plus x (S y)) = S (plus y (S x)) Holes: Comm.rhs4 *Comm>
複雑ですね。
このような場合は、plusの中にあるSを、外へはじき出せないか考えてみましょう。
再び標準ライブラリから、plusSuccRightSuccという関数を探し出します。
*Comm> :t plusSuccRightSucc plusSuccRightSucc : (left : Nat) -> (right : Nat) -> S (left + right) = left + S right Holes: Comm.rhs4 *Comm>
いけそう...ですが、左辺と右辺が逆ですね。このような場合は、関数symをかましましょう。
Sを外へはじく箇所は二つあるので、二回連続で rewrite します。
comm : (x, y : Nat) -> x + y = y + x comm Z Z = Refl comm (S x) Z = rewrite plusZeroRightNeutral x in Refl comm Z (S y) = rewrite plusZeroRightNeutral y in Refl comm (S x) (S y) = rewrite sym (plusSuccRightSucc x y) in rewrite sym (plusSuccRightSucc y x) in ?rhs4
*Comm> :l Comm Type checking ./Comm.idr Holes: Comm.rhs4 *Comm> :t rhs4 x : Nat y : Nat _rewrite_rule : plus x (S y) = S (plus x y) _rewrite_rule1 : plus y (S x) = S (plus y x) -------------------------------------- rhs4 : S (S (plus x y)) = S (S (plus y x)) Holes: Comm.rhs4 *Comm>
おしい！ x と y が逆です。
でもあきらめてはいけません。実はもう解けているのです。
hoge : x -> T x を証明したい時、
hoge Z と
hoge (S x) に分けたとすると、
hoge (S x) のところでは、hoge x が使えるのです。
定理証明の分野でも、再帰は有効なのです。
今回の場合だと、(comm x y)（型はx + y = y + x）が使えます。
最後に、両辺にS Sがかかっていますが、これには関数congを使います。
関数congと、{}で囲む暗黙の引数については、今回は説明しません。
comm : (x, y : Nat) -> x + y = y + x comm Z Z = Refl comm (S x) Z = rewrite plusZeroRightNeutral x in Refl comm Z (S y) = rewrite plusZeroRightNeutral y in Refl comm (S x) (S y) = rewrite sym (plusSuccRightSucc x y) in rewrite sym (plusSuccRightSucc y x) in cong {f = S . S} (comm x y)
*Comm> :l Comm Type checking ./Comm.idr *Comm>
Hole が全て消えて、これにて証明完了です。
ソースコード全体
Ruby で型検査
やってみた。
型検査に使う gem が Ruby2.6 を要求しているので、それをインストールする。
Linux(Ubuntu) です。
git
$ git clone https://github.com/rbenv/rbenv.git ~/.rbenv
$ git clone https://github.com/rbenv/ruby-build.git ~/.rbenv/plugins/ruby-build
.bashrc や .bash_profile などに以下の記述を追加
export PATH="$HOME/.rbenv/bin:$PATH"
eval "$(rbenv init -)"
インストール可能な Ruby のバージョンを確認
$ rbenv install -l
$ rbenv install --list-all | grep 2.6
おまじない
$ sudo apt install libssl-dev
インストール
$ CONFIGURE_OPTS='--disable-install-rdoc' rbenv install 2.6.0
$ rbenv global 2.6.0
おまけ
「2.6.0」を「3.0.0-preview1」に変えれば、最新版の Ruby が試せる。
Steep
$ gem install steep
適当に「fizz」というフォルダを作る。
その中に「fizzbuzz.rb」「fizzbuzz.rbs」「Steepfile」を配置する。
「fizzbuzz.rb」は以下。普通の FizzBuzz です。
# 単純な REPL ならこれで十分 # $ ruby fizzbuzz.rb # irb なら # $ irb # > load 'fizzbuzz.rb' # > fizz(50) def fizz(n) (1..n).each{|k| if k % 15 == 0 p "FizzBuzz" elsif k % 3 == 0 p "Fizz" elsif k % 5 == 0 p "Buzz" else p k end } end # メイン関数としたもの if __FILE__ == $0 fizz(50) end
「Steepfile」は以下。
target :test do typing_options :strict check "*.rb" signature "*.rbs" end
なんかでたー $ steep check fizzbuzz.rb:11:6: NoMethodError: type=self, method=p (p "FizzBuzz") fizzbuzz.rb:13:6: NoMethodError: type=self, method=p (p "Fizz") fizzbuzz.rb:15:6: NoMethodError: type=self, method=p (p "Buzz") fizzbuzz.rb:17:6: NoMethodError: type=self, method=p (p k) fizzbuzz.rb:23:15: FallbackAny ($0) fizzbuzz.rb:24:2: NoMethodError: type=::Object, method=fizz (fizz(50))
今日はここまで。
（続きやらないかも......）
参考記事
Ubuntu で最新版の Ruby をインストール
https://qiita.com/kerupani129/items/77dd1e3390b53f4e97b2
macOS で Ruby 3.0.0-preview1 をインストール（Homebrew の ruby-build を使わない方法も）
https://qiita.com/scivola/items/ac83d8275ace1b4ed123
Ruby の型関連の情報まとめ
https://qiita.com/natsuokawai/items/6d652e3b72a79e019f22
