ラムダ式→SKIコンビネータ項

概要

ラムダ式をSKIコンビネータの式に変換するプログラムを書きました。
koba-e964/ski-comb · GitHub

やったこと

ラムダ式→SKIコンビネータの項の変換

実装は
高階ことりちゃんと学ぶSKIコンビネータ
を参考にしました。

例

Haskell風の書き方で説明します。やり方は上のリンク先に書いてあるので、ここでは実例だけ紹介します。
C = \x y z -> x (y z)
をSKIコンビネータ項に直してみましょう。
(1) 全てのλ抽象を新しく導入した関数に直す。このとき、新しく導入される関数の定義は、
関数名 自由変数... ラムダ式で束縛される変数
の形になる。
まずトップレベルの\x->...を直しましょう。

C = M
M x = \y z -> x (y z)

続いてM xの内部の\y -> ...を直します。

C = M
M x = N x
N x y = \z -> x (y z)

同様にして最終的には以下のようになります。

C = M
M x = N x
N x y = O x y
O x y z = x (y z)

(2) 関数の引数を消去してS,K,Iのみで表す
O x y z = x (y z)
O x y z = (K x z) (y z)
O x y z = S (K x) y z
O x y = S (K x) y
O x = S (K x)
O x = (K S x) (K x)
O x = S (K S) K x
O = S (K S) K

C=M=N=O*1より、結局
C = S (K S) K
がわかる。

課題


ここのやり取りで気付いたのですが、今のままだと実行時間も出力されるコードも線型よりも速いペースで増大します。現在のところどのくらいのペースで増大するのか見積もりができていないので、

  • 計算量・出力されるコードの大きさの増大の速さの見積もり
  • 高速化・サイズ削減

が目標になるかと思います。

*1:実際のコードではここもちゃんとやっているのでコードが肥大化します

ICPC 2014 Domestic

ICPC 2014 DomesticにAyatakaというチーム名で参加しました。
(メンバ:ばいなり(b_inary), うどん(kw_udon_), こば(kobae964))

A
うどんがやってくれました

B
私がやりました( Ideone.com - 2gTylp - Online C++ Compiler & Debugging Tool )

C
ばいなりがやってくれました

D
うどんと私がやりました ( Ideone.com - bJqf8d - Online C++ Compiler & Debugging Tool )

E
ばいなりがやってくれました

F
全員で考えました。
貪欲に残り回数が一番多い方向へ転がすという方針でやったら失敗しました。コンテスト終了後に7完したチームに解法を聞いたらあざやかでびっくり。

G
捨てました

こんな感じで5完13位( ACM-ICPC 2014 国内予選順位表 )でした。選ばれなかったAyataka(>_<)

モナド変換子の圏論的理解(Categorical understanding of monad transformers)

モナド変換子

Haskellにおいてモナド変換子(Monad transformer)は、以下の条件を満たすtです:

  • tのkindは(* -> *) -> * -> *
  • lift :: Monad m => m a -> t m aが定義されている
  • liftが以下の法則を満たす:
    1. lift . return = return
    2. ∀m k. lift (m >>= k) = lift m >>= (lift . k)

(この定義を便宜上函数的定義(functional definition)と呼びます。)
この定義を圏論の言葉を使って書きなおすことを考えると、以下のようになります:

  • tのkindは(* -> *) -> * -> *
  • lift :: Monad m => m a -> t m aが定義されている
  • liftが以下の法則を満たす:
    1. liftはmからt mへの自然変換(natural transformation)になっている。つまり、
      • ∀(k :: a -> b). fmap k . lift = lift . fmap k
    2. liftはEndofunctorの圏におけるモノイド対象の準同型である。つまり、以下が成立する:
      • lift . return = return (単位元を保つ)
      • lift . join = join . fmap lift . lift (積を保つ)

(この定義を便宜上圏論的定義(categorical definition)と呼びます。)

この二つの定義が同値であることを示します。

函数的定義→圏論的定義

(1) lift . return = return
(2) ∀m k. lift (m >>= k) = lift m >>= (lift . k)
を仮定する。

(i) ∀(k :: a -> b). fmap k . lift = lift . fmap k

(2)においてk=return . fを代入すると
∀m f. lift (m >>= return . f) = lift m >>= (lift . return . f)
∀m f. lift (m >>= return . f) = lift m >>= (return . f) ((1)より)
fmap f m = m >>= return . fを利用すると
∀m f. lift (fmap f m) = fmap f (lift m)
∀f. lift . fmap f = fmap f . lift (mを消去)

(ii-i) lift . return = return

(1)から自明。

(ii-ii) lift . join = join . fmap lift . lift

(2)にk=idを代入すると
∀m. lift (m >>= id) = lift m >>= (lift . id)
m >>= id = join m, idは恒等射より
∀m. lift (join m) = lift m >>= lift
m >>= k = join (fmap k m)より
∀m. lift (join m) = join (fmap lift (lift m))
mを消去して
lift . join = join . fmap lift . lift

圏論的定義→函数的定義

読者の演習問題とする。(訳:疲れました)

追記(2014/06/25)要望があったので答えを載せます。(白い文字で書いているので選択すると読めます)
(i) ∀(k :: a -> b). fmap k . lift = lift . fmap k
(ii-i) lift . return = return
(ii-ii) lift . join = join . fmap lift . lift
を仮定する。

(1) lift . return = return

(i)から自明。

(2) ∀m k. lift (m >>= k) = lift m >>= (lift . k)

(以下白文字)

(i)の両辺に左からjoin . fmap liftを合成して
∀k. join . fmap lift . fmap k . lift = join . fmap lift . lift . fmap k
(ii-ii)を右辺に適用して
∀k. join . fmap lift . fmap k . lift = lift . join . fmap k
fmap (g . f) = fmap g . fmap fより
∀k. join . fmap (lift . k) . lift = lift . join . fmap k
両辺をmに適用して
∀m k. join (fmap (lift . k) (lift m)) = lift (join (fmap k m))
m >>= k = join (fmap k m)を利用して変形すると
∀m k. lift m >>= lift . k = lift (m >>= k)

Haskellでのエラー処理について(ErrorT, ExceptT)

Haskellでインタプリタ( https://github.com/koba-e964/experiment/tree/master/typeinf )を書いていて、エラー処理をしたくなったのでモナド変換子ErrorTを導入しました。その後別の環境でコンパイルしてみたら

(前略) Use Control.Monad.Except instead (後略)

 と怒られてしまったのでびっくりして確認すると、どうやらmtlのバージョンがエラー処理を書いた環境は2.0以前、別の環境では2.2.0.1(2.2.1かも？記憶があいまい)だったのが原因だったようです。

このControl.Monad.Exceptというモジュールは、ここ2週間くらい前(2014/6/2)にリリースされたmtl-2.2.1 ( http://hackage.haskell.org/package/mtl-2.2.1 )で新たに導入されたようです。

 

新しく導入されたモナド変換子ExceptTと、以前からあったErrorT (Control.Monad.Error)との違いですが、見たところ型変数eに関する制約が無くなったというのが唯一の違いであるように思われます。ErrorTの各種インスタンス宣言には、

(Monad m, Error e) => MonadError e (ErrorT e m)

(Monad m, Error e) => Monad (ErrorT e m)

のように、Error eという宣言が必要でしたが、ExceptTのインスタンス宣言には必要ありません。(例:

Monad m => MonadError e (ExceptT e m)

Monad m => Monad (ExceptT e m)

など)