Try SLC を公開しました
SLCをWebブラウザ上で実行できるTry SLC(Symmetric Lambda Calculus)を公開しました。
SLCって？
SLCとはSymmetric Lambda Calculusの略で、日本語だと対称ラムダ計算と呼ばれる、ラムダ計算の一種です。
その名の通り対称性が特徴なラムダ計算です。
ここで言う対称性は、値(これまでの計算結果)と継続(残りの計算)におけるもので、関数と組(ペア)において値と継続を対称性を持って同じように扱うことができます。
要は値の否定が継続で、関数には対偶があって、ド・モルガンです！
と言う説明ではわからないので元のSLCの論文 "Declarative Continuations and Categorical Duality" (Filinski 1989) か、
関連した日本語の論文 "型付き対称λ計算の基礎理論" (阪上 2008) を読みましょう。(ぶん投げ)
ちなみに以下で"値"と書いているものはお茶大の論文では"項"にあたるので注意して下さい。(Filinskiの方では"value"なので"値"と書いてます。お茶大の方では"値"は"項"のそれ以上簡約できない形を指すのに使っています。)
Try SLC
Try SLCはSLCをJavaScriptで動くようにして、Webブラウザで動作を試すことができる環境です。
実際にはFilinskiの論文の付録のCamlでの実装をF#で書き直し、さらにFunScriptというF#→JavaScriptコンパイラによってJavaScriptのコードを生成しています。
使い方
ページ下部の入力欄にSLCの式、または変数名:=SLCの式と入力し、右の丸いボタンを押すかShift+Enterを押すことで実行します。
SLCの式を入れた場合にはその式を評価して結果を返し、変数名:=SLCの式を入れたときは式を評価した結果で変数を定義します。
文法
基本的な文法は先の論文を読んでもらうとして、いくつか論文中の表記と相違点があるので書いておきます。
変数の定義
前述の使い方で書いた通り変数名:=SLCの式で変数が定義できます。
元の実装ではzdにあたる動作です。
関数の表記
関数の表記に用いられる⇒および⇐は、=>および<=になります。
再帰関数はrec 識別子=本体のままです。
関数適用の表記
関数適用に用いられる↑および↓は、^および?になります。
関数の値扱い継続扱い(及びその逆)
関数の値扱い及びその逆⌈⋅⌉, ⋅と、関数の継続扱い及びその逆⌊⋅⌋, ⋅は、論文中でさらっと
In the SLC, explicit conversions between the three syntactic classes are not necessary in the concrete syntax, but are present as implied operators in the abstract one.
とあるように実際には出てきません。
構文においてある部分で要求されるのが値か継続か関数(か値引数か継続引数か)か分かる(例えば値が要求される部分でf^xとあったらfは関数でxは値である必要があるというように上から順次決まっていく)ので、それに従いこれらの変換が付けられます。
既知のバグ
6/8:修正しました。
原因は生成されたJavaScriptで関数を呼び出した結果が保存されず、何度も同じ呼び出しをしていた部分があった為でした。
複雑な式を入れると結果が待てど暮らせど返ってこなくなります。
例えばpf := f<=n=>(r<={r?(()=>1), r?(()=>n*f^(n-1))})^(n=0)とかやると死にます。(この式は元の論文での実行例にでている式)
どうやら型推論のあたりで問題が起きてるっぽいんですが原因まだ特定できてません。
前述した通り、Try SLCはF#で書いたインタプリタからJavaScriptに変換してその上で動いており、元のF#実装では問題なく動いているので色々謎です。
そのうち治します。治せたらいいな。
