- 421 名前：１３２人目の素数さん mailto:sage [2009/08/08(土) 15:26:39 ]
- Church-Rosserの定理を簡単な場合（型のないλ計算）でいいので、形式的
（1階の述語論理）に証明してみようかななんて思ってるんですけど、特に
文字列の置換を形式化するのって難しくないですか？関数記号とか、述語記号を
どのように定めればいいでしょうか。どなたかアドバイスしていただけませんか。
（集合論の形式化だと述語は∈とか＝くらいでよかったんだけど、もしや、かなり
たくさんの関数記号、述語記号が必要になるんでしょうか。）
