解決可能 - mrsekut-p

解決可能

resolvable

ラムダ抽象に何かを付け加えてIコンビネータに簡約できたら、解決可能

定義

ラムダ式$ Mが以下のいずれかを満たすとき、解決可能という

$ Mがコンビネータであるとき、次式を満たす$ n個のラムダ式$ N_1,N_2,\cdots,N_nが存在する

$ MN_1N_2\cdots N_n\xrightarrow{\ast}_\beta I

つまり、ラムダ抽象$ M何かを付け加えてIコンビネータに簡約できたら、解決可能なんやなmrsekut.icon

$ Mを、コンビネータ$ \lambda x.Mとしたときに、「$ \lambda x.M」が解決可能である

解決可能でないラムダ抽象のことを「解決不能(unsolvable)」と言う