状態を持つラムダ計算(1) - エレファント・ビジュアライザー調査記録

ChatGPTに入力してみることの続きです。今のところ自分でプログラムを書くぐらいの入力をしてもプログラムをちゃんと書いてくれないし、自分で証明を書くぐらいの入力をしても証明をちゃんと書いてくれないという状況です。今はやり方が書かれた本がいろいろ出ているのでできるようになっているかと思いましたが、今のところこのようなやり方が書かれた本は見つかりません。しかしいずれはそのようなことが書かれた本も出るのではないかと思います。それまではこのブログも意味があるので、それはそれで良いです。自分が何かを考えるときのヒントにはなるので、ここではその方針でやっていきます。

関数型言語について質問するよりもラムダ計算について質問した方がちゃんと答えてくれる感じがしました。そこで、いったんクロージャーについて質問するのはやめて、ラムダ計算について質問してみます。

以下のように入力しました。

ラムダ計算について教えてください

ラムダ計算を行うプログラミング言語を定義して、その構文を教えてください

ラムダ計算で変更可能な変数を扱うにはどうすれば良いですか

「参照セル」、「状態モナド」などの答えが返ってきました。クロージャーについて調べるには「参照セル」の方が良いかもしれませんが、まず、「状態モナド」について質問してみます。

状態モナドを持つラムダ計算を行うプログラミング言語を定義してください

状態モナドを持つラムダ計算を行うプログラミング言語のプログラムを、状態モナドを持たないラムダ計算を行うプログラミング言語のプログラムに書き直すことはできますか

以下は引用です。

はい、状態モナドを持つラムダ計算を行うプログラミング言語のプログラムを、状態モナドを持たないラムダ計算を行うプログラミング言語のプログラムに書き直すことは可能ですが、その書き直しはいくつかの制約や変更を伴うことがあります。
状態モナドを持つラムダ計算を行うプログラミング言語では、状態を取得する `get` 関数と状態を設定する `set` 関数が提供されます。一方、状態モナドを持たないラムダ計算を行うプログラミング言語では、変更可能な状態を扱うための特別な構文や関数が提供されないため、状態を取得または設定する方法が異なる可能性があります。
以下は、状態モナドを持つラムダ計算を行うプログラミング言語の例と、それを状態モナドを持たないラムダ計算を行うプログラミング言語に書き直した例です。
状態モナドを持つラムダ計算を行うプログラミング言語の例（Haskell風）
-- 状態モナドを持つラムダ計算を行うプログラミング言語の例

type State s a = s -> (a, s)

-- 状態を取得する関数
get :: State s s
get s = (s, s)

-- 状態を設定する関数
set :: s -> State s ()
set s _ = ((), s)

-- ラムダ抽象
lam :: (a -> State s b) -> State s (a -> b)
lam f s = (\x -> fst (f x s), s)

-- 関数適用
app :: State s (a -> b) -> State s a -> State s b
app f x s = let (fn, s') = f s
                (arg, s'') = x s'
            in (fn arg, s'')

-- 使用例
example :: State Int Int
example = do
    set 5
    f <- lam (\x -> get)
    x <- get
    return (f x)
状態モナドを持たないラムダ計算を行うプログラミング言語に書き直した例
-- 状態モナドを持たないラムダ計算を行うプログラミング言語の例

-- 変数とラムダ抽象のみの単純なラムダ計算を定義
data Exp = Var String | Lam String Exp | App Exp Exp

-- ラムダ抽象内での変数の束縛を行う関数
lam :: String -> Exp -> Exp
lam v e = Lam v e

-- 関数適用を行う関数
app :: Exp -> Exp -> Exp
app e1 e2 = App e1 e2

-- 使用例
example :: Exp
example = app (lam "x" (Var "x")) (Var "y")
このように、状態モナドを持つラムダ計算を行うプログラミング言語の構文や関数を、状態モナドを持たないラムダ計算を行うプログラミング言語に書き直すことは可能ですが、それぞれの言語の特性や機能に応じて適切な書き直しを行う必要があります。

Haskell については詳しくないのですが、有限の回数で終了するプログラムのようです。有限の回数で終了する場合は書き直すことができると思われるので、聞きたいことはそういうことではありません。Haskell の本や、ウェブの入門的記事に書かれている例は、だいたい有限の場合です。これはなんとかならないかと思います。ただしこの場合は大丈夫なのかもしれませんが、Haskell には精通していないので、今後調べていきたいと思います。

次は以下のことをやってみたいと思います。