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

プログラミング言語 idris

これは Theorem Prover Advent Calendar 2016 17日目の記事として書かれました.

idrisは依存型を持つ純粋関数型プログラミング言語です. ちなみにアイコンはこんな感じ.

f:id:wkwkes:20161215155232p:plain *1

今月の初め, バージョン 0.99 がリリースされました. 機能もほぼ安定したといことで これを機に少し遊んでみたのでその紹介をします.

はじめに断っておきますが, 私自身 idris を触って間もないのでおかしなことを書いている可能性があります. 間違い等あれば指摘していただければ幸いです.

処理系

brew install idris などで降ってきます. idris でREPLが起動します.

$ idris
     ____    __     _
    /  _/___/ /____(_)____
    / // __  / ___/ / ___/     Version 0.99
  _/ // /_/ / /  / (__  )      http://www.idris-lang.org/
 /___/\__,_/_/  /_/____/       Type :? for help

Idris is free software with ABSOLUTELY NO WARRANTY.
For details type :warranty.
Idris>

ghciに近い感覚で使えます. 複数行入力は :let でできますが, やりにくいので一度ファイルにプログラムを記述してそれを読み込むのが無難だと思います. 実行ファイルが欲しければコマンドラインからidris -o hoge hoge.idr などとすればOKです.

基本構文

だいたい Haskell です. 型クラス相当のものやdo-notation まであります. 例えば 標準入力から受け取った文字列をそのまま出力するプログラムは次のように書けます.

main : IO ()
main = do x <- getLine
          putStrLn x

Haskellっぽいですね.

Haskell と違うところは Idris for Haskellers にまとまっていますが, すぐ気になるのは例えば

  • 評価が正格
  • ::: が逆
  • 関数の型の記述が原則必須

などでしょうか.

また, 前述した通り idris には依存型があります.

たとえば伝統的な, 長さの情報をもつリストは次のように定義できます.

data Vect : Nat -> Type -> Type where
  Nil : Vect Z a
  (::) : a -> Vect k a -> Vect (S k) a

Vect 上の関数として例えば head を書いておきます.

head : Vect (S n) a  -> a
head (x :: _) = x

依存型・証明

依存型といえば Coq や Agda が有名ですが, 定理証明支援系としての側面の強いそれらに対して, idris は依存型を用いた(通常の)ソフトウェア開発の可能性を探ることを目標にしているそうです.

とは言っても依存型がある以上, 証明的なものを書く必要が出てきます. たとえば次の reverse 関数を考えます.

reverse : Vect n a -> Vect n a
reverse x = reverse_ x Nil
  where
    reverse_ : Vect n a -> Vect m a -> Vect (n + m) a
    reverse_ Nil ys = ys
    reverse_ (x :: xs) ys = reverse_ xs (x :: ys)

よさそうに見えますが, コンパイルすると怒られます.

When checking right hand side of Main.reverse, reverse_ with expected type
        Vect (S k + m) a

Type mismatch between
        Vect (k + S m) a (Type of Main.reverse, reverse_ a n x_shadow k (S m) xs (x :: ys))
and
        Vect (plus (S k) m) a (Expected type)

Specifically:
        Type mismatch between
                plus k (S m)
        and
                S (plus k m)

コンパイラplus k (S m)S (plus k m) が等しくないと言っています. 愛くるしいですね.

ここでplus k (S m)S (plus k m) が等しいことを証明する必要がありますが, idris の証明はいくつか方法があります.

  • 示したいことを型にもつプログラムを直接書く.
    • 一番直接的な証明です. エディタのプラグインを使えば意外とシュッとかけます.
  • 対話的に証明する.
    • Coq のように対話的に証明を行えます. REPLから
      • :elab
      • :p

      のどちらかをタイプすることで対話環境に入ることができます. :elab は elaborator という idris に埋め込めるDSL的なもののスクリプトを生成します. :p も似たような証明のスクリプトを生成しますが現バージョンでは既に非推奨*2になっています.

証明のやり方がいくつかあって戸惑いますが, 少し触ってみたところ, 等式の証明をするときはプログラムを直接書くのがやりやすい. elaborator は構文が大げさで使いにくい. :p から入る証明モードが一番使いやすいと感じました. 遊んだ程度なので話半分に思ってください.

とりあえず plus k (S m)S (plus k m) が等しいことを :elab で証明してみます. そのためにはまず証明する箇所をプログラム中に明示する必要があります.

reverse : Vect n a -> Vect n a
reverse x ?= reverse_ x Nil
  where
    reverse_ : Vect n a -> Vect m a -> Vect (n + m) a
    reverse_ Nil ys = ys
    reverse_ (x :: xs) ys ?= reverse_ xs (x :: ys)

?= に注意してください. これが証明する箇所を表します. 上のプログラムをREPLで実行すると

Idris> :l test.idr
Holes: Main.reverse_lemma_1, Main.reverse__lemma_1

となって, ?=に書き換えた証明すべきところが Holes になっています. idris では不完全な定義などが Holes として明示されます. REPLで :m とすれば Holes の一覧を見ることができます.

今から tactic を用いて Hole を埋めていくことになります.

まず Main.reverse_lemma_1 を埋めましょう. :elab コマンドで証明用のシェルに入ります.

*test> :elab Main.reverse_lemma_1


----------                 Goal:                  ----------
{hole0} : (a : Type) ->
          (n : Nat) -> Vect n a -> Vect (n + fromInteger 0) a -> Vect n a

Goal や 仮定 がでてきます.

tactic の詳細は :doc <tactic> を見てください. 一気にやります. 雰囲気を感じてもらえれば.

-Main.reverse_lemma_1> intro'

----------              Assumptions:              ----------
 a : Type
----------                 Goal:                  ----------
{hole0} : (n : Nat) -> Vect n a -> Vect (n + fromInteger 0) a -> Vect n a
-Main.reverse_lemma_1> intro'

----------              Assumptions:              ----------
 a : Type
 n : Nat
----------                 Goal:                  ----------
{hole0} : Vect n a -> Vect (n + fromInteger 0) a -> Vect n a
-Main.reverse_lemma_1> intro'

----------              Assumptions:              ----------
 a : Type
 n : Nat
 x : Vect n a
----------                 Goal:                  ----------
{hole0} : Vect (n + fromInteger 0) a -> Vect n a
-Main.reverse_lemma_1> compute

----------              Assumptions:              ----------
 a : Type
 n : Nat
 x : Vect n a
----------                 Goal:                  ----------
{hole0} : Vect (plus n 0) a -> Vect n a
-Main.reverse_lemma_1> rewriteWith `(plusZeroRightNeutral ~(Var `{{n}}))

----------              Assumptions:              ----------
 a : Type
 n : Nat
 x : Vect n a
----------                 Goal:                  ----------
{hole0} : Vect (plus n 0) a -> Vect (plus n 0) a
-Main.reverse_lemma_1> attack
----------              Other goals:              ----------
{hole0}
----------              Assumptions:              ----------
 a : Type
 n : Nat
 x : Vect n a
----------                 Goal:                  ----------
{hole1} : Vect (plus n 0) a -> Vect (plus n 0) a
-Main.reverse_lemma_1> intro'
----------              Other goals:              ----------
{hole0}
----------              Assumptions:              ----------
 a : Type
 n : Nat
 x : Vect n a
 value : Vect (plus n 0) a
----------                 Goal:                  ----------
{hole1} : Vect (plus n 0) a
-Main.reverse_lemma_1> fill (Var `{{value}})
----------              Other goals:              ----------
{hole0}
----------              Assumptions:              ----------
 a : Type
 n : Nat
 x : Vect n a
 value : Vect (plus n 0) a
----------                 Goal:                  ----------
{hole1} : Vect (plus n 0) a =?= value
-Main.reverse_lemma_1> solve

----------              Assumptions:              ----------
 a : Type
 n : Nat
 x : Vect n a
----------                 Goal:                  ----------
{hole0} : Vect (plus n 0) a -> Vect (plus n 0) a =?= \value => value
-Main.reverse_lemma_1> solve
reverse_lemma_1: No more goals.

証明が終わったら:qedコマンドで証明が出力されるのでそれをソースコードに貼り付ければ以降証明の必要はありません.

-Main.reverse_lemma_1> :qed
Proof completed!
Main.reverse_lemma_1 = %runElab (do intro'
                                    intro'
                                    intro'
                                    compute
                                    rewriteWith `(plusZeroRightNeutral ~(Var `{{n}}))
                                    attack
                                    intro'
                                    fill (Var `{{value}})
                                    solve
                                    solve)

Main.reverse__lemma_1 も同じ要領でやった結果ソースコードは次のようになります.

reverse : {n: Nat} -> Vect n a -> Vect n a
reverse x ?= reverse_ x Nil
  where
    reverse_ : {n: Nat} -> {m: Nat} -> Vect n a -> Vect m a -> Vect (n + m) a
    reverse_ Nil ys = ys
    reverse_ (x :: xs) ys ?= reverse_ xs (x :: ys)

Main.reverse_lemma_1 = %runElab (do intro'
                                    intro'
                                    intro'
                                    compute
                                    rewriteWith `(plusZeroRightNeutral ~(Var `{{n}}))
                                    attack
                                    intro'
                                    fill (Var `{{value}})
                                    solve
                                    solve)

Main.reverse__lemma_1 = %runElab (do intro'
                                     intro'
                                     intro'
                                     intro'
                                     intro'
                                     intro'
                                     intro'
                                     intro'
                                     compute
                                     rewriteWith `(plusSuccRightSucc ~(Var `{{k}}) ~(Var `{{m}}))
                                     attack
                                     intro'
                                     fill (Var `{{value}})
                                     solve
                                     solve)

型が通るのが確認できます.

Idris> :l test.idr
*test>

以上が :elab による証明の例でした.

対話的証明ではなく直接プログラムを書くスタイルのプログラム例も書いておきます.

とりあえず Reading HoTT in Coq の Coq のプログラムを参考に id : A -> AA の間の equivalence になることを示してみました. (余分な関数も含まれています)

なお, 等式の証明についての詳しい説明は The Idris Tutorial: Thorem Proving などにあります.

total
inverse : {A: Type} -> {x, y: A} -> (x = y) -> (y = x)
inverse Refl = Refl

total
concat : {A: Type} -> {x, y: A} -> {z: A} -> (x = y) -> (y = z) -> (x = z)
concat Refl Refl = Refl

total
concat_p1 : (A: Type) -> (x: A) -> (y: A) -> (p: x = y) -> (concat p Refl = Refl{x = x})
concat_p1 A x x Refl = Refl{x = (Refl{x = x})} 

total
inv_inv : {A: Type} -> {x, y: A} -> (p: x = y) -> (inverse (inverse p)) = p
inv_inv Refl = Refl

total
concat_assoc : (A: Type) -> (x: A) -> (y: A) -> (z: A) -> (w: A) -> (p: x = y) -> (q: y = z) -> (r: z = w) -> ((concat p (concat q r)) = (concat (concat p q) r))
concat_assoc A x x x x Refl Refl Refl = Refl

total
transport : {A: Type} -> {x, y: A} -> (P: A -> Type) -> (p: x = y) -> (u: P x) -> (P y)
transport P Refl u = u

total
ap : {A, B: Type} -> {x, y: A} -> (f: A -> B) -> (p: x = y) -> (f x = f y) 
ap f Refl = Refl

total
apD : {A: Type} -> {B: A -> Type} -> {x, y: A} -> (f: (a: A) -> B a) -> (p: x = y) -> transport _ p (f x) = f y
apD f Refl = Refl

total
sect : {A, B: Type} -> (A -> B) -> (B -> A) -> A -> Type
sect s r x = r (s x) = x

record IsEquiv (A: Type) (B: Type) (f: A -> B) where
  constructor BuildIsEquiv
  equiv_inv : B -> A
  eisretr : (x: B) -> sect equiv_inv f x
  eissect : (x: A) -> sect f equiv_inv x
  eisadj : (x: A) -> eisretr (f x) = ap f (eissect x)

record Equiv (A: Type) (B: Type) where
  constructor BuildEquiv
  equiv_fun: A -> B
  equiv_isequiv: IsEquiv A B equiv_fun

total
idmap : (A: Type) -> A -> A
idmap A = \ x : A => x

isequiv_idmap : (A: Type) -> IsEquiv A A (idmap A)
isequiv_idmap A = BuildIsEquiv (idmap A) (\ _ : A => Refl) (\ _ : A => Refl) (\ _ : A => Refl)

equiv_idmap : (A: Type) -> Equiv A A
equiv_idmap A = BuildEquiv (idmap A) (isequiv_idmap A) 

concat_p1Refl の型が推論してもらえず少し手こずりましたが, 他はすんなりいったと思います.

その他の話題

バックエンドがいろいろある

バックエンドというよりコンパイルのターゲットという方がいいかもしれません. Language Reference: Code Generation Targets にまとまっています. ここにも書き写しておきます.

Malfunction を経由して OCaml のバックエンドを利用する話は少し話題になっていた記憶があります.

エディタ

emacs, vim , atom あたりにはプラグインがあります. 型を書くとその実装の雛形を生成してくれたり, 簡単な証明を探索してくれたりして便利です. 詳しい説明は Theorem Proving: Pattern Matching Proofs にあります.

ちなみに私は emacs の idirs-mode を使いました.

おわりに

プログラミング言語の紹介と言いながら構文にほぼ言及しないなどよくわからない記事になりましたが, 参考になれば幸いです.

最後に参考にした・参考になりそうなページをあげて終わります.

LLVMのOCaml bindingをためす

前からLLMVが気になっていて, きつねさんの本 をざっと読んだりしたが手を動かしてなかったのでチュートリアルをやることにした.

LLVM Tutorial: Table of Contents — LLVM 3.8 documentation

古いチュートリアルだということは知っていたが他にないので仕方なくやってみた.*1

現在の環境(LLVM3.8)でやるのは厳しかった. 途中までだがせっかくなのでメモしておく.

好みでC++ではなくOCamlを選んだ.

LLVMC++で書かれているがOCamlのbindingが公式でサポートされている. 雑に検索したところOCaml以外にHaskell, Go, Rustなどにもbindingがあるらしい.

そういえばRustの初期のコンパイラOCamlLLVMで作られていたみたいな話があった気がする.


コード

ビルドするにはLLVM(3.8)とOCamlの各種ライブラリ(llvm, ctypes, (ppx_deriving))とocamlbuildが必要. 4章の分までは一応動くが後で述べるように色々問題がある.

github.com


やったこと

1章・2章

字句解析と構文解析で, 特にLLVMに関係がない.

構文解析, 字句解析ともにCamlp4をバリバリ使っているけど, 今はppxが推奨されるらしいのでどうなのかという気がする.

私はocamllexとmenhirを使った.

3章

ここからLLVMを使う.

3章では抽象構文木からLLVM IRという中間コード生成をする. そのままコンパイルしようとするとaddやmulでdoubleを使ってることを怒られる. faddやfmulに書き換えてdoubleをfloatにするとコンパイルできる.

4章

最適化のためにパスをいくつか入れて, そのあとJITで動かす.

4章のコードをビルドしようとすると

Error: Unbound module ExecutionEngine

になる. ググると同じエラーが出てる人が多い.

3.8にはそもそもLlvm_executionengine.ExecutionEngineなるモジュールがない. 3.5まではあるみたいなので, LLVMのバージョン3.6のリリースノート を見ると

LLVM 3.5 has, unfortunately, shipped a broken Llvm_executionengine implementation. In LLVM 3.6, the bindings now fully support MCJIT, however the interface is reworked from scratch using ctypes and is not backwards compatible.

ということらしい.

パスはとりあえず諦めてJITで動かすことを目標にした. 名前と型とモジュールの説明からそれっぽい関数を探して書き換えていくと一応動いた.

# 1 + 1;                                                                                                                            
                                                                                                                                    
define float @"00"() {                                                                                                              
entry:                                                                                                                              
  ret float 2.000000e+00                                                                                                            
}                                                                                                                                   
                                                                                                                                    
Evaluated to 2. 
# def foo(a b) a*a + 2*a*b + b*b;                                                                                                   
                                                                                                                                    
define float @foo(float %a, float %b) {                                                                                             
entry:                                                                                                                              
  %fmultmp = fmul float %a, %a                                                                                                      
  %fmultmp1 = fmul float 2.000000e+00, %a                                                                                           
  %fmultmp2 = fmul float %fmultmp1, %b                                                                                              
  %faddtmp = fadd float %fmultmp, %fmultmp2                                                                                         
  %fmultmp3 = fmul float %b, %b                                                                                                     
  %faddtmp4 = fadd float %faddtmp, %fmultmp3                                                                                        
  ret float %faddtmp4                                                                                                               
}                                                                                                                                   
                                                                                                                                    
                                                                                                                                    
# foo(2,3);                                                                                                                         
                                                                                                                                    
define float @"00"() {                                                                                                              
entry:                                                                                                                              
  %calltmp = call float @foo(float 2.000000e+00, float 3.000000e+00)                                                                
  ret float %calltmp                                                                                                                
}                                                                                                                                   
                                                                                                                                    
Evaluated to 25. 

それでもまだ色々問題がある

  • 無名関数が実行できない(チュートリアル通り無名関数の名前を""にしてるとexception Llvm_executionengine.Error("Function not found")になる
  • トップレベルのexpressionの評価が一度しか行えない(二度目はエラーになる)
  • extern cosなどで宣言した関数が正しく動かない

とりあえず無名関数にも内部では名前("00")をつけたり, 一度トップレベルのexpressionを評価するたびにllmoduleを作り直したりすることでそれっぽい挙動にはなるが, 評価のたびに関数の定義が消えるというような他の問題が生じる.

5章以降では構文も増えてこのまま進むのは無理そうなので一旦OCamlを離れてC++LLVMを知るのが先だなという気持ちになってきた.


感想

OCamlだけでLLVMを始めるのは厳しい


その他

構文解析木をプリントするのに初めてppx_derivingを使ってみたら便利だった. 今まで書いてきた手書きプリンターはなんだったのか.

# def foo(a b c) (a - b) * (b - c) + (c - a);   
                                                                                    
(Ast.Def                                                                                                                            
   Ast.Function (Ast.Prototype ("foo", [|"a"; "b"; "c"|]),                                                                          
     Ast.Binary_c ("+",                                                                                                             
       Ast.Binary_c ("*",                                                                                                           
         Ast.Binary_c ("-", (Ast.Variable "a"), (Ast.Variable "b")),                                                                
         Ast.Binary_c ("-", (Ast.Variable "b"), (Ast.Variable "c"))),                                                               
       Ast.Binary_c ("-", (Ast.Variable "c"), (Ast.Variable "a")))))                                                                

参考にしたもの

*1:この段階で古かったようなので相当 OCaml で LLVM -- 事始め - Oh, you `re no (fun _ → more)

ラムダ計算の評価器とBöhm tree

気持ち

『きつねさんでもわかるLLVM』を読んだので何か書いてみようと思い, 一回書いておくかというのもあってラムダ計算の評価器を書くことにしました. 書いた結果, LLVMを使っても仕方ないことに気がついた(遅い!) のでLLVMはつかっていません. ついでにBöhm treeを出力させることにしました.

Böhm tree

ググると詳しく解説したPDFなどが見つかるので簡単に書きます.

任意のラムダ項は

  1. { \displaystyle
\lambda x_0 . \cdots \lambda x_n . x M_0 M_1 \cdots M_m \ \ (n, m \geq 0)
}
  2. { \displaystyle
\lambda x_0 . \cdots \lambda x_n . (\lambda x M) M_0 \cdots M_m \ \ (n \geq 0 , m \geq 0)
}

のどちらかの形にかけます*1. 1 を頭正規形といい, 2 の{ \displaystyle (\lambda x M) M_0}という部分を頭基といい, 頭基をβ簡約することを頭変換といいます. あるラムダ項が頭正規形をもつなら頭変換だけで頭正規形に変換できることが知られています.

これらの性質を使ってラムダ項を木として表現したものをBöhm tree といいます. 以下が定義です.

ラムダ項{M}

  • 頭正規形の形のとき, BT({M}) = 親 : { \displaystyle \lambda x_0 . \cdots \lambda x_n . x }, 子 : BT({M_0}), {\cdots}, BT({M_m})

  • 2の形のとき, 頭正規形になるまで頭変換を繰り返します. 頭正規形にならないときは無限木は書いていられないので BT({M}) {= \bot}とします.

これらを繰り返すことで得られる木がBöhm treeです.

コード

出力の形式をどうするか考えましたが, 手軽さと, ひょっとしていつか使えるかもしれないと思い{\displaystyle \LaTeX}のコードとして出力することにしました. 木を表示には tikz-qtree*2というパッケージをつかいました.*3.

C++で書きました. 良いC++書き方がわからないので変なことをしている可能性があります. 定義通りではないのですが, 正規形があるかわからない場合はある程度繰り返して止まるようになっています.

github.com

出力された{\displaystyle \LaTeX}のコードから出力された結果です. 入力とともに出力されています.

f:id:wkwkes:20160309221223p:plainf:id:wkwkes:20160309221230p:plainf:id:wkwkes:20160309221236p:plainf:id:wkwkes:20160309221242p:plainf:id:wkwkes:20160309221249p:plain

参考にした本

Amazon CAPTCHA

字句解析器・構文解析器, ASTの設計を参考にしました.

Amazon CAPTCHA

De Brujinインデックスのあたりを参考にしました.

Amazon CAPTCHA

http://pauillac.inria.fr/~levy/courses/tsinghua/lambda/3-5/lecture3-5-4.pdf

Böhm treeの参考にしました.

*1:ここで帰納法が回る

*2:CTAN: Package tikz-qtree

*3:パッケージの仕様上あまり深い木は出力できないみたいです

Billiard-ball computer

Billiard-ball Computerという計算モデルがあると知った。
Billiard-ball computer - Wikipedia, the free encyclopedia
ボールの存在で1と0をあらわし、うまく衝突させることで論理回路を作るというものである。チューリング完全性があるらしい。

具体的には、摩擦がなく完全弾性衝突するという条件下で、二つのボールを入力とみなせば、以下のような衝突でANDを構成することができる。
f:id:wkwkes:20150719021709p:plain

あと、NOTがほしいが、これらはANDほど単純には構成できない。
Conservative logic - Springerを見るとFredkin gateと呼ばれる回路を使えばいいらしい。

そのためにまず、Switch gateと呼ばれる以下の回路を考える。*1
f:id:wkwkes:20150719021925p:plain

左から入力し、右へ出力する時をオレンジで、右から入力し、左へ出力する時を青で表した。

これを4つ用いると以下のようにFredkin gateが構成出来る。
f:id:wkwkes:20150720212255p:plain

代入すると確かめられるが、Fredkin gateの真ん中の出力は、

  • Q=0 のとき (C\wedge P) \vee (\neg C \wedge Q) = C \wedge P
  • P=0 かつ Q = 1のとき (C\wedge P) \vee (\neg C \wedge Q) = \neg C

などとなる。
2つ目の性質からNOTが得られる。

以上でANDとNOTが構成できたので、Billiard-ball Computerがチューリング完全であることが確かめられた。

3DCGを作る環境があったので以上のこと使って、NOTとXORをCGでシミュレートしようと試みた。

物理演算でやろうとしたところ、回路が長くなるとどうしても思い通りの挙動を取らなかったため、シミュレーションは諦めて、理想上のモデルの動く様子を動画にした。

それぞれNOTに対して、1と0を入力した様子を表す。

Fredkin gate を4つ合わせて作ったXORに1と0を入力した様子を表す。レンダリングのミスで見にくいが、たしかに1を出力している。

*1:Switch gateとFredkin gateの構成は一例にすぎず、同じ挙動をとればどんな構成でもいいみたい。