意義のある意味論的マッピングは決定可能か？

Question

この質問の私の貧しい表現のために謝罪、私はそれを適切に尋ねる語彙を持っているか分からない。

私は（ごく最近）

⟦let x = x in x⟧ = ⊥ 

に似て何かを書きましたが、本当に私はここでトリッキーな何かを理解するために失敗しています。私はこのステートメントが本当に⊥であると主張することができます。なぜなら、それは非生産的な無限ループだからです。さらに、私は

⟦let ones = 1:ones in ones⟧ = μ(λx.(1,x)) = (1, (1, (1, ...))) 

のようなものを主張することができますが、その中に何が入っていますか？おそらく、それは無限の数の "1と3つのタプル"、完全に明確な数学的なオブジェクトであれば、AFAには問題ありませんが、どうすれば有限個の "1と3つのタプル"そして非生産的なのは⊥？

明らかに、これは停止問題に答えることを含むため、一般的にはできません。

したがって、セマンティックマッピングが完全な関数であるかのように計算するにはどうすればよいですか？チューリング不完全な言語ではセマンティクスが必ずしも非決定論的であるか？私はそれは、意味論が常に言語のおおよその非公式な記述であることを意味すると考えていますが、この「穴」はさらに進んでいますか？

Answer 1

チューリング完全言語の理論モデルはありません。あなたの言語が強く正規化されている場合は、「解釈する」機能があります。あなたは、非チューリング完全言語で理論セマンティクスを設定してもしなくてもよい。いずれにせよ、完全なチューリングと完全ではないチューリングの言語は、トータル・セマンティック・マッピング機能で理論的セマンティクスを設定することはできません。

私はそれがここで問題ではないと思います。

帰納的定義と誘導的定義には違いがあります。私たちは、理論的には、このセットを探索することができます：

を整数のリストの誘導定義が読み取ります

セット[Z]が最小は、空のリストがSにあるようSを設定し、そのようなのためにということです任意のlsのSおよびnのZの対(n,ls)のS。

これはまた、あなたが[Z] = \Union_{i \in N}([Z](n)を定義することができます[Z](0) = {[]}と[Z](n) = {(n,ls) | n \in Z, ls \in [Z](n-1)}として「ステップインデックス化」方法で提示することができます（あなたが自然数で信じるならば！）

一方Haskellでは、「リスト」 最大は、FORALLことSに設定されているより密接coinductively

セット[Z]（coinductive）で定義される「coinductiveストリーム」に関連していますのS,x = []またはx = (n,ls)のnのZおよびlsのSである。

つまり、コインシデンス定義は後方にあります。帰納的定義はいくつかの要素を含む最小の集合を定義しますが、すべての要素が特定の形を取る最大の集合を定義します。

誘導リストの長さが有限であることを示すのは簡単ですが、誘導リストの中には無限に長いものがあります。あなたの例は共導入が必要です。

より一般的には、帰納的定義は「ファンクタの最低固定点」とすることができ、一方、共導の定義は「ファンクタの最大の固定点」と考えることができます。ファンクタの「最小の固定点」は「初期代数」であり、「最大の固定点」は「最終的な結合点」です。これをセマンティックツールとして使用すると、セットのカテゴリ以外のカテゴリで物を定義しやすくなります。

私はHaskellはこれらのファンクタを記述するための優れた言語を提供することを見つける

data ListGenerator a r = Cons a r | Nil 

instance Functor (ListGenerator a) where 
    fmap f (Cons a x) = Cons a (f x) 
    fmap _ Nil  = Nil 

その関数空間がCBNで、言語がトータルではありませんので、Haskellは、これらのファンクタを記述するための優れた言語を提供するが、我々はありません持っています我々は最大の不動点

data GF f = GF (f (GF f)) 

や実存

を定量化した非再帰の定義を取得んが、我々は:(たい少なくとも固定ポイントの種類を定義する方法

data GF f = forall r. GF r (r -> (f r)) 

我々は厳しいか総言語で働いていた場合には、少なくとも不動点は普遍的に定量化

data LF f = LF (forall r. (f r -> r) -> r) 

EDIT次のようになります。「最小」は「少なくとも」/」いえセット理論的な概念であるため、 「最大の」区別は正しいものではないかもしれない。 LFの定義は、基本的にGFと同形であり、「最小の固定点」の形式的形式である「自由初期代数」である。

私はそれが「1-とタプル」のいくつかの有限数と、非生産的⊥ではないことを納得させることができる方法

のよう？

私はこの投稿の構造の種類を信じていない限り、あなたはできません。もし私がしたら、あなたの定義は私を立ち退かせてしまう！ "onesは、ペアで構成された誘導ストリームであると言う場合は、(1,ones)"私は信じなければならない！私はonesが定義によって_|_ではないことを知っています。したがって、誘導によって、どの値でもnは私にはnのものがあり、その後は底になることはできません。私は、あなたの主張を否定しようとすることができるのは、共生蒸気の存在を否定することだけです。 http://www.cs.ox.ac.uk/people/daniel.james/unique/unique-tech.pdf

Answer 2

は、あなたがHinzeとジェームズ 『正しい証明ユニークな固定小数点の原理』を見てみることができます。 2番目の例で$ \ mu $ではなく$ \ nu $であってはなりません。 （あなたは最大の固定点を取っています、これはHaskellで起こっていることです）