η-変換
出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2021/04/12 16:37 UTC 版)
上に挙げた2つの規則の他に、第3の規則としてイータ変換が導入されることがある。イータ変換の基本的なアイデアは、関数の外延性である。ここでいう外延性とは、2つの関数が全ての引数に対して常に同じ値を返すようなとき、互いに同値であるとみなすという概念である。イータ変換は以下の変換である。 λV. E V →η E ただし、 E に V が自由出現しないときに限る。 この同値性は関数の外延性という概念によって以下のように示される。 もし全てのラムダ式 a に対して f a == g a であるならば、 a として f にも g にも自由出現しない変数 x をとることによって f x == g x であり、 λx. f x == λx. g x である。この等式にイータ変換をほどこすことによって f == g が得られる。これより、イータ変換を認めるならば関数の外延性が正当であることが示される。 逆に、関数の外延性を認めるとする。まず、全ての y に対してラムダ式 (λx. f x) y はベータ変換でき、 (λx. f x) y == f y となる。この同値関係は全ての y について成り立っているので、関数の外延性より λx. f x == f である。以上によって、関数の外延性を認めたときのイータ変換の正当性が示される。
※この「η-変換」の解説は、「ラムダ計算」の解説の一部です。
「η-変換」を含む「ラムダ計算」の記事については、「ラムダ計算」の概要を参照ください。
ウィキペディア小見出し辞書の「η-変換」の項目はプログラムで機械的に意味や本文を生成しているため、不適切な項目が含まれていることもあります。ご了承くださいませ。
お問い合わせ。
- η-変換のページへのリンク
