Explicit substitution とは

コンピュータサイエンスでは、ラムダ計算は、置換プロセスの形式化に特別な注意を払うならば、明示的な置換を持つと言われています。これは、置換がベータ還元によって暗黙的に行われ、計算内では表現されない標準的なラムダ計算とは対照的である。明示的置換の概念は、正式な記述と置換のすべての数式の実装で概念が頻繁に(暗黙的かつ明示的に)現れるため、(全く異なる性質を持つ文献に明示的に置換された多数の公表された計算の計算にもかかわらず)抽象機械、述語論理、記号計算などの変数を含む。