帰納的定義 - pogi-log

帰納的定義

帰納的定義(きのうてきていぎ、Inductive definition)

無限の場合について厳密な定義をするためには、帰納的(inductive) 定義が用いられる。帰納的定義とは「基底の場合」と「前の定義から 1 つ進めた場合」について定義を与えることで、あらゆる正の n について「基底の場合から n 個進めた場合」を定義する方法である。

帰納的定義の大枠

主に最初の定義と後続ステップの2種類がある?

最初のステップ/基底ステップ(initial step/base step)

構成を始めるにあたっての出発点

後続ステップ/帰納ステップ(sccessor step/induction step)

それまでのステップで構成されたものを処理して、新しいものを作るステップ

自然数の帰納的定義(Coqバージョン)は以下のような記法

code:coq

-- 自然数の帰納的定義

Inductive nat : Set :=

| O : nat

| S : nat -> nat.

BNF記法は文法などを帰納的に定義するためによく使われる記法

確認用

Q. 帰納的定義