Simply Typed Lambda CalculusのRust実装

概要

このリポジトリは、Rust言語によって実装された「Simply Typed Lambda Calculus（単純型付きラムダ計算）」のインタープリターです。元々の非型付きラムダ計算のプロジェクトを発展させ、STLCの型システムを取り入れたことで、型安全な関数計算のモデルをコードとして体験できます。Lexer（字句解析器）で文字列をトークン化し、Parser（構文解析器）で抽象構文木（AST）を生成、その後型検査を行い、型の整合性を保ちながら評価器で式を実行します。Rustの型システムと強力なパターンマッチングを活用し、教育的かつ実践的にラムダ計算の基礎を学べる設計です。

リポジトリの統計情報

• スター数: 2
• フォーク数: 0
• ウォッチャー数: 2
• コミット数: 4
• ファイル数: 6
• メインの言語: Rust

主な特徴

• Simply Typed Lambda Calculusの型システムをRustで実装
• Lexerによるトークン化とParserによるAST生成
• 型検査機能で型安全性を保証
• 評価器で型付けされたラムダ式の実行が可能

技術的なポイント

本プロジェクトの最大の特徴は、単純型付きラムダ計算（STLC）をRustで丁寧に実装している点にあります。STLCはラムダ計算に型の概念を導入し、型安全なプログラムの理論的基盤として知られています。リポジトリはその理論を実践的なコードに落とし込み、STLCの学習教材としても利用可能な設計です。

まず、入力された文字列をLexerでトークン化し、計算式の構文要素に分解します。この字句解析はRustの列挙型やイテレータで効率的に構築されており、入力の検証やエラー検出を支援します。次にParserがトークン列から抽象構文木（AST）を生成し、計算の構造を表現します。ASTはRustのEnumで表され、関数抽象（λ式）、変数、適用などのノードを厳密に型付けしています。

さらにSTLCの核心である型検査は、ASTに対して型環境を用いて再帰的に型推論・検証を行います。これにより、型の不整合や誤用をコンパイル時に検出し、誤ったラムダ式の評価を防止します。Rustの強力な型システムとパターンマッチングが、この処理の実装を簡潔かつ安全にしています。

最後に評価器は、型検査を通過したASTを実際に評価し、関数適用の結果を計算します。STLCの性質上、評価が型安全であることが保証されているため、実行時の型エラーが起こりません。これにより、教育的な観点からもSTLCの動作を追体験しやすくなっています。

全体として、Rustのモダンな言語機能を活用しつつ、単純型付きラムダ計算の理論と実装を結びつけたことが本リポジトリの技術的なハイライトです。

プロジェクトの構成

主要なファイルとディレクトリ：

• .gitignore: ファイル除外設定
• Cargo.lock: Rust依存関係ロックファイル
• Cargo.toml: プロジェクト設定ファイル
• README.md: プロジェクト概要と使い方の説明
• assets: ロゴなどの画像ファイルを格納

その他のファイル：

• srcディレクトリ（推定）：Lexer、Parser、型検査、評価機能のRustコードが格納されていると推測されます。

まとめ

RustでSTLCを体系的に学べる良質な教材的リポジトリ。

リポジトリ情報：

• 名前: simply-typed-lambda-calculus
• 説明: 説明なし
• スター数: 2
• 言語: Rust
• URL: https://github.com/z4nder/simply-typed-lambda-calculus
• オーナー: z4nder
• アバター: https://avatars.githubusercontent.com/u/39275291?v=4