ベータ簡約
読み：ベータかんやく

　ラムダ計算における変換規則の一つ。ラムダ式の中の各ラムダ項同士の関係を定めたものである。
目次
基本理念
概念
　ラムダ計算においても関数の適用という概念がある。
　つまり式を書き換えて簡単にする規則を定めたものがベータ簡約である。
表現
　(λx.M)
　は、写像x→Mを表わす。つまり入力xに対しMを返すとことを表現するラムダ項とされる。
　(MN)
　は、ラムダ項Mにラムダ項Nを渡す、あるいはMにNを適用するということを表現するラムダ項である。このMやNは具体的には(λx.K)や(x+1)などのラムダ項となることもある。
　また括弧は適宜省かれる。
例
　次の式は、xにNを入力し、その上でそのxに対しMを返すと言う意味である。
　(λx.M)N
　さらにいうとA=(λx.M)などとしてANはNをAに適用しAを返すと言うことができる。
　このような意味を式の書き換えであらわす。
操作
β-redex
　次の形になっているものをβ-redexと呼ぶ。
　((λx.M)N)
　この形においてNをxに代入し(xをNに書き換え)て式を簡単にすることができる。これをベータ簡約という。
例
　(λx.x2+1)(y+1)
　はβ-redexの形を持っていて(上項目例ならM=x2+1、N=y+1)、
　λy.(y+1)2+1
　にベータ簡約できる。
注意
　この書き換えにおいて式の意味が変わってしまってはいけない。
　たとえば
　(λx.x2+y)(y+1)
　などを考えるとき、
　λy.y2+y
　としてしまえば、(λx.x2+y)のyは自由変数なのに、書き換え後は束縛変数になってしまい、式の意味が変わってしまう。
　よってこのような事態にはならぬよう、適宜アルファ変換を行なってからベータ簡約をする。
正規形
　ベータ簡約がこれ以上できない、つまりβ-redexと呼ばれる形が式中に存在しないラムダ式を正規形という。
再検索