式

完全な構文

式の詳細については後述しますが、まずはこれが何であるかを明らかにするために、以下に文字列と nat リテラルの拡張を含む式についての完全な構文を挙げます：

Expr ::= 
  | boundVariable 
  | freeVariable 
  | const 
  | sort 
  | app 
  | lambda 
  | forall 
  | let 
  | proj 
  | literal

BinderInfo ::= Default | Implicit | InstanceImplicit | StrictImplicit

const ::= Name, Level*
sort ::= Level
app ::= Expr Expr
-- a deBruijn index
boundVariable ::= Nat
lambda ::= Name, (binderType : Expr), BinderInfo, (body : Expr)
forall ::= Name, (binderType : Expr), BinderInfo, (body : Expr)
let ::= Name, (binderType : Expr), (val : Expr) (body : Expr)
proj ::= Name Nat Expr
literal ::= natLit | stringLit

-- Arbitrary precision nat/unsigned integer
natLit ::= Nat
-- UTF-8 string
stringLit ::= String

-- fvarId can be implemented by unique names or deBruijn levels; 
-- unique names are more versatile, deBruijn levels have better
-- cache behavior
freeVariable ::= Name, Expr, BinderInfo, fvarId

これについて、いくつかの注意点があります：

  • nat リテラルが利用する Nat は任意精度の自然数・bignum でなければなりません。
  • 束縛子（ラムダ・pi・let・自由変数）を持つ式では3つの引数（束縛子の名前・型・スタイル）を1つの引数 Binder として簡単にまとめることができます。ここで束縛子は Binder ::= Name BinderInfo Expr となります。他の場所で例示する疑似コードでは、読みやすさのためにそのプロパティを持っているかのように常に扱うことにします。
  • 自由変数の識別子は、一意な識別子にすることも de Bruijn レベルにすることもできます。
  • Lean で使用される式の型は mdata コンストラクタというものも持っており、これはメタデータを付与した式を宣言します。このメタデータはカーネル内での式の動作には影響しないため、このコンストラクタはここでは取り扱いません。

束縛子の情報

ラムダ・pi・let・自由変数コンストラクタで構築された式は、名前・束縛子の「スタイル」・束縛子の型の形式で束縛子の情報を保持します。束縛子の名前とスタイルはプリティプリンタが使用するためだけのものであり、推論・簡約・同値チェックの中核となる処理を変更することはありません。しかし、プリティプリンタでは束縛子のスタイルがプリティプリンタのオプションに応じて出力を変更することがあります。例えば、ユーザは暗黙的または暗黙インスタンス（型クラス変数）を出力に表示したい場合もあれば、したくないこともあるでしょう。

ソート

sort は単にレベルのラッパーであり、式として使用することができます。

束縛変数

束縛変数は de Bruijn インデックス を表す自然数として実装されています。

自由変数

自由変数は束縛子が一時的に利用できない状況で、束縛変数に関する情報を伝達するために使用されます。これは自由変数について、新しい（異なる場合もある）束縛変数に入れ替えて束縛子を再構築する上で束縛変数を一時的に自由変数に置き換える代わりに、カーネルが束縛式の本体を走査し、束縛情報の構造化されたコンテキストを保持しないことを通常選択するためです。この利用できないことの説明は曖昧に聞こえるかもしれませんが、役立つように文字通りに説明すると、式は親ノードのポインタを持たない木として実装されているため、子ノードに降りてくると（特に関数の境界を超える場合）、ある式の現在地より上の要素を見失ってしまうことになってしまいます。

束縛子を再構築して開いた式を閉じる時、束縛子が変更されることで以前に有効だった de Bruijn インデックスが無効になることがあります。一意な名前か de Bruijn レベルを使用することで、あらゆる変更を補正し、再束縛された変数の新しい de Bruijn インデックスが再構築されたテレスコープに対して有効であることを保証するようにこの束縛子を再度閉じることができます（この節 を参照してください 1）

今後、実装がどのようなスキーム（一意なIDか de Bruijn レベル）を使っているかに関わらず、何らかの形で「自由変数の識別子（free variable identifier）」という用語を使うかもしれません。

const

const コンストラクタは、ある式が環境内の別の宣言を参照するための方法です。これは参照として行われなければなりません。

以下の例では、def plusOne が Definition 宣言を作成し、これがチェックされたのちに環境に受け入れられます。こうした宣言は式の中に直接置くことはできないため、plusOne_eq_succ の型が前の宣言 plusOne を呼び出すときは名前を指定しなければなりません。こうして Expr.const (plusOne, []) という式が作成され、カーネルがこの const 式を見つけると、plusOne という名前で参照されている宣言をこの環境で探すことができます：

def plusOne : Nat -> Nat := fun x => x + 1

theorem plusOne_eq_succ (n : Nat) : plusOne n = n.succ := rfl

const コンストラクタで作成された式は、const 式が参照する定義を検索することで、環境から取得した宣言の展開や推論に代入されるレベルのリストも保持します。例えば、const List [Level.param(x)] の型を推測するには、現在の環境で List の宣言を検索し、その型と宇宙パラメータを取得し、そして List が最初に宣言された宇宙パラメータに x を代入します。

ラムダ式、pi

lambda と pi 式（Lean では pi の代わりに forallE を使用します）は、それぞれ関数の抽象化と「全ての」束縛子（依存関数型）を意味します。

   束縛子名        本体
      |            |
fun (foo : Bar) => 0 
            |         
         束縛子の型

-- `BinderInfo` は束縛子を囲む括弧のスタイルに反映されています。

let 式

let はまさにその名前の通りのものです。let 式は束縛子ですが、BinderInfo を持たず、束縛子の情報は Default として扱われます。

   束縛子名        値
      |            |
let (foo : Bar) := 0; foo
            |          |
        束縛子の型      .... 本体

適用

app 式は関数への引数の適用を表します。適用のノードはバイナリ（2つの子、つまり1つの関数とその1つの引数のみを持つ）であるため、f x_0 x_1 .. x_N は App(App(App(f, x_0), x_1)..., x_N) として表され、以下のような木として視覚化されます：

                App
                / \
              ...  x_N
              /
            ...
           App
          / \
       App  x_1
       / \
     f  x_0

カーネルが提供する式の操作は非常に一般的で、適用の列を畳み込んだり展開したりすることで、上の木構造から (f, [x_0, x_1, .., x_N]) を取得したり、f, [x_0, x_1, .., x_N] を上の木へと畳み込んだりすることができます。

射影

proj コンストラクタは構造体の射影を表します。再帰的でなく、コンストラクタが1つしかなく、添字を持たない帰納型は構造体になることができます。

このコンストラクタは当該の型の名前と、射影されるフィールドを示す自然数、そして射影が適用される実際の構造体を取ります。

ここでカーネルでは射影のインデックスは 0 始まりであるのに対して Lean の用語では 1 始まりであることに注意してください。Lean サイドでは 0 はそのコンストラクタのパラメータではない最初の引数に使われます。

例えば、proj Prod 0 (@Prod.mk A B a b) というカーネルの式は、パラメータ A と B をスキップした後の0番目のフィールドとして a を射影します。

proj が提供する動作は、型の再帰子を使用することで実現できますが、proj は頻繁に行われるカーネルの操作をより効率的に処理します。

リテラル

Lean のカーネルはオプションとして任意精度の Nat リテラルと String リテラルをサポートしています。必要に応じてカーネルは自然数リテラル n を Na.zero または Nat.succ m に変換したり、文字列リテラル s を String.mk List.nil や String.mk (List.cons (Char.ofNat _) ...) に変換したりすることができます。

文字列リテラルは、定義上の等しさをテストするためか、再帰子の簡約において主要な対象として現れる時に文字のリストに遅延変換されます。

自然数リテラルは文字列を同じ立ち位置（定義上の等しさと再帰子の適用の主要な対象）でサポートされていますが、カー熱は加算・乗算・指数・減算・剰余・割り算のほか、自然数リテラルに対する真偽値の同値と「以下」の比較もサポートしています。

1

訳注：原文では./kernel_concepts.md#implementing-free-variable-abstractionへリンクが貼られていましたがリンクが切れていたので対応するリンクに更新しています。