帰納的型

帰納的型(inductive type)

型がどういうものかを定義する感じのもの

帰納的型は以下の4つの推論規則を持つようになっている

1. 構成規則 (formation rule)

2. 構成子 (constructor)

3. 除去子 (eliminator)

4. 計算規則 (computation rule)

1. 構成規則 (formation rule)

構成規則はその型がとるパラメータなどを指定

2. 構成子 (constructor)

その型の要素を作るための定数や関数

3. 除去子 (eliminator)

その型から他の型への関数を作るもの

帰納法原理 (induction principle) とも呼ばれる

4. 計算規則 (computation rule)

除去子に構成子を適用したときにどのように簡略されるかという規則

Coqの帰納型は以下のような記法

code:coq

-- 自然数の帰納的定義

Inductive nat : Set :=

| O : nat

| S : nat -> nat.

Lean 4の場合

code:Lean4

inductive <型名> : Type

| <要素1> : <型名>

| <要素2> : <型名>

:

| <要素N> : <型名>

これは列挙型

code:Lean4

inductive Weekday where

| sunday : Weekday

| monday : Weekday

| tuesday : Weekday

| wednesday : Weekday

| thursday : Weekday

| friday : Weekday

| saturday : Weekday

確認用

Q. 帰納型

関連

参考

メモ

Coq

Lean 4