α-変換
出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2021/04/12 16:37 UTC 版)
アルファ変換の基本的なアイデアは、束縛変数の名前は重要ではない、ということにある。例えば、 λx. x と λy. y は同じ関数を表している。しかし、ことはそう単純ではない。ある束縛変数の名前を置換してもよいかどうかには、いくつかの規則が絡んでくる。例えば、ラムダ式 λx. λy. x 中の変数 x を y に置き換えると、 λy. λy. y となるが、これは最初の式とはまったく異なるものを表すことになる。そこでまず準備として、変数 V, W と式 E に対して、 E 中の V の全ての自由出現を W に置き換えたものを E[V := W] と書くことにする。この元で、アルファ変換は λV. E →α λW. E[V := W] である。ただし、 E に W が自由出現しておらず、かつ V を置換することにより E 中で新たに W が束縛されることがないときに限る。この規則によれば、式 λx. (λx. x) x が λy. (λx. x) y に変換されることがわかる。
※この「α-変換」の解説は、「ラムダ計算」の解説の一部です。
「α-変換」を含む「ラムダ計算」の記事については、「ラムダ計算」の概要を参照ください。
ウィキペディア小見出し辞書の「α-変換」の項目はプログラムで機械的に意味や本文を生成しているため、不適切な項目が含まれていることもあります。ご了承くださいませ。 お問い合わせ。
- α-変換のページへのリンク
