ラムダ計算の勉強

このゼミでは，本研究室において必要なラムダ計算という数理言語について，教科書*1を用いて，基礎からこれを習得することを目的としています．

よって，専門的な予備知識の必要なく，このゼミで研究に必要な考え方を学んでいます．

関連する学部の講義には，論理学，コンパイラ，オートマトン等があり，これらを履修してあると，学習がスムーズに行えます．

このゼミで用いる教科書は，第1部(アルゴリズム)と第2部(プログラミング言語)に分かれていますが，ここでは第2部について読み進めることになります．以下に，この教科書の主なトピックを紹介します．

§10　プログラミング言語の概要

勉強をするにあたって，基礎となる集合に関する記法を学びます．

• 直積や直和などの基本的なものから，同値関係，反射的推移的閉包などの定義について，問を交えながら．

§11　シンタックスの定義と解析

言語に必要な語彙・文法の定義，そしてそれを解析する方法の概要について書かれています．

• 正規言語・正規表現での語彙の定義，文脈自由文法による文法の定義．
• 有限状態機械による字句解析，LR構文解析法による構文解析．

§12　型付きラムダ計算

この章から，学部の講義では扱わないラムダ計算について，その定義等を学べます．

• ラムダ式の定義，その型の解析(自然演繹システム，ラムダ式の型システム)，意味論について，問を解きながら．
  • 解く方法は帰納法が主．数学的帰納法と考え方は似ています．

§13　種々の構文構造の表現

§14　プログラム実行のモデル

この章では，ラムダ式によって表現されたプログラムを計算機で実行する，3つの方法について書かれています．

• 実行環境に依存せずにラムダ計算を実現する，コンビネータ理論について．
  • コンビネータと対応する，ヒルベルトシステムについて．
  • ラムダ式とコンビネータの関係，コンビネータの実行．
• 環境を用いて変数の束縛を実現する自然意味論について．
  • 自然意味論の評価関係，ラムダ式と自然意味論の関係．
• SECD機械による自然意味論の実現について．
  • SECD機械の実行規則，ラムダ式のSECDコードへの翻訳，自然意味論とSECD機械の実行の関係．

§15　型の自動推論と型の多相性

（文責：菊池）