/lambda-friends

Web上で動作するラムダ計算のインタプリタ「らむだフレンズ」

Primary LanguageTypeScriptMIT LicenseMIT

らむだフレンズ

CircleCI MIT License

純粋型なし λ 計算と、型付き λ 計算（FL）のインタプリタです。

※現在メンテナンスのため、GUI の型付きモードを一時的に無効化しています。

GitHub Pages 上に置いてあるのでそちらが標準の環境です が、git cloneしてから手元のブラウザでdocs/index.htmlを開いても動きます。

今できること

  • 純粋型なし λ 計算と、型付き λ 計算（FL）を扱える（設定により変更可）
  • それぞれの推論規則に基づいた簡約ができる
    • 型なしの場合、η 簡約の可否を設定できる。
    • 型なしの場合、簡約基を選択して簡約を進められる。
    • 型なしの場合、評価戦略の指定ができる。
  • マクロ定義ができる
    • 「マクロ」タブで定義済みマクロの一覧を表示する
  • マクロ定義を書き並べたファイルを読み込める
    • Lambda*Magicaとの後方互換性あり。*.lm.txt（の形式のプレーンテキスト）を読み込める。
  • LaTeX 形式で出力ができる（「Export」タブ）
    • 型推論の証明木（bussproofs 形式、型付きのみ）
    • 簡約の途中経過
  • 入力履歴を補完できる
    • Linux のターミナルのように、上キーを押すと履歴を表示する。
    • 静的 javascript なので、セッションを超えて遡ることはできない。
    • localStorage を使い、セッションを越えて遡れるようになった。
  • チャーチ数とチャーチ真理値の判定が出来る
    • 簡約後の形がチャーチ数・チャーチ真理値の場合、そのように表示
  • 簡約グラフの表示ができる
    • 「グラフ」タブで簡約グラフを表示
    • Cytoscape.jsを利用
    • 多重辺はオン・オフ選択可能
    • png 形式の画像としてダウンロード可能
  • LMNtal グラフと相互に変換できる
    • 「Import」「Export」タブ
    • エンコーディング方式は後述
    • 型なしのみ
  • SKI コンビネータと相互に変換できる
    • SKI → ラムダ は組み込みマクロとして
    • ラムダ → SKI は Export タブに
  • de Bruijn Index と相互に変換できる
    • de Bruijn → ラムダ は Import タブに
    • ラムダ → de Bruijn は Export タブに
  • 簡約グラフの形からラムダ式を逆引きできる（実験機能）
    • 「Import」タブ
    • まだ実験なので完全性はないが、健全性はある

基本的な入力形式

  • 「\」「¥」「λ」はすべて「λ」として解釈される
  • 関数適用は左結合的に解釈される
  • λ 抽象は最長一致で解釈される
  • 以上 2 つをもって曖昧性が排除される場合、括弧は省略して良い
  • 空白は無視される
  • 変数に使用できるのは大小英文字（計 52 文字）のみ。

マクロ定義

Lambda*Magicaと同様の形式でマクロ定義ができる。

マクロは、 false = \xy.yのように定義し、 <false>のように使う。

型なしの場合、未定義のマクロは式中で使用できるが、自由変数と同様に扱われる（簡約基とみなされない）。

型付きの場合、未定義のマクロは式中で使用できない。

また、型付きで定義したものは型付きでしか使用できない（逆も然り）。

組み込みマクロ

以下の 3 つは、定義せずとも利用できる。ユーザ定義のマクロはこれらの名前を使用できない。

  • チャーチ数 ex. <3> <5>
  • チャーチ真理値 <true> <false>
  • SKI コンビネータ <S> <K> <I>

FL で新たに導入された構文

角括弧 [ ] で囲まれたキーワードは、型付き λ 計算（FL）のキーワードとして解釈する。

  • 基本型
    • 整数(int)型 ex. [-1] [2531]
    • 論理(bool)型 ex. [true] [false]
  • 基本型に対する組み込み演算（2 項演算、前置演算子）
    • int -> int -> int型 ： [+] [-] [*] [/] [%]
      [/]は切り捨て後の商、[%]は余りを返す。
    • int -> int -> bool型 ： [<] [>] [<=] [>=] [==] [!=]
    • bool -> bool -> bool型 ： [eq] [and] [or] [xor] [nand] [nor]
  • 空リスト [nil]
  • 式（expression）
    • [if] M [then] M [else] M
    • [let] x=M [in] M
    • [case] M [of] [nil] -> M | x::x -> M
  • 不動点演算子 [fix]

LMNtal コードへの変換について

型なしモードで入力されたラムダ式を、階層グラフ書き換え言語 LMNtalの式に自動的に変換する。エンコーディング方式は以下の論文のものを採用。

  1. Kazunori Ueda, Encoding the Pure Lambda Calculus into Hierarchical Graph Rewriting. Proc. RTA 2008, LNCS 5117, Springer, 2008, pp.392-408.

CLI モードの動かし方（デバッグ用）

Node.js（nodeコマンド）と TypeScript（tscコマンド）がグローバルに使える環境が必要です。

$ git clone https://github.com/nikosai/lambda-friends.git
$ cd lambda-friends
$ npm i
$ ./run.sh

すると、対話モード（REPL）が起動します。詳しい操作方法は、:? または :h で表示されるヘルプを参照してください。

また、実行時オプションを付けることもできます。使用できるオプションは、./run.sh -hで表示されます。

特に、./run.sh -i "<2><2>" のようにすると、ワンライナーで実行ができます。

その他

  • このプロジェクトは、MIT ライセンスでコードを公開しています。
  • このプロジェクトは、Lambda*Magicaに影響を受けて始動しました。
  • 上記のロゴは、けものフレンズ ロゴジェネレータで作成しました。
  • 動作報告・フィードバックを歓迎します → Twitter: @nikosai2531
  • バグ報告は Issue を投げてください。