問題タブ [denotational-semantics]

ここで説明されているHaskellのBottomは、エラーがある、終了していない、または無限ループを含む任意のタイプの計算であると言われています...これはHaskellに固有のものですか? 格子理論ではそこの概念もあることを知ってBottomいます...定義された順序に基づいてBottomを定義するべきではありませんか?

不滅の言葉をフィーチャーしたTシャツが販売されていたことを誓います。

のどの部分

分かりませんか？

私の場合、答えは...すべてです！

特に、Haskellの論文ではこのような表記がよく見られますが、それが何を意味するのかわかりません。数学のどの分野になっているのかわかりません。

もちろん、ギリシャ文字の文字と「∉」（通常、何かが集合の要素ではないことを意味します）などの記号を認識します。

一方、私はこれまで「⊢」を見たことがありません（ウィキペディアはそれが「パーティション」を意味するかもしれないと主張しています）。ここでの括線の使用にも慣れていません。（通常、それは分数を示しますが、ここではそうではないようです。）

誰かが少なくとも、このシンボルの海が何を意味するのかを理解するためにどこから始めればよいかを教えてくれるなら、それは役に立ちます。

私は言語仕様を書いていますが、次の初歩的な質問を解決する必要があります。(明らかに不自然な) 抽象構文があるとします。

この言語の表示的セマンティクスはどのように見えますか? 非終端記号は「<」と「>」で囲み、終端記号は囲みません。1...6を自然数の定義域にマッピングしたい。私にはまったく明確ではないことは、非端末にマッピングを提供する必要があるかどうかです。<A> ::= <B> | <C>たとえば、意味がないので、そうする必要はないようです。それは単なる構造の一部です。今のところ、このルールを完全に排除できることは無視してください。

したがって、現状では、これは完全な表示定義が次のように見えるべきだと私が考えるものです。ここで、右側 (イタリック体) は自然数からの対応する値を表します。

[[1]] =1

[[2]] =2

[[3]] =三

[[4]] =四

[[5]] =五

[[6]] =六

A美学的には、 、B、またはまったく言及しないのは奇妙に思えCますが、これらの記号は実際のプログラム(: など4) には決して現れないので、これで十分かもしれません。この主題に関する私が持っているすべての資料は、この非常に単純で基本的な言語定義プロセスの側面を議論から省略しています。

私は、表示セマンティクスの概念について少し混乱しています。私が理解しているように、表示セマンティクスは、関数と式が特定のプログラミング言語でどのように機能するかを記述することになっています。これらの機能とその働きを説明するために使用される適切な形式は正確には何ですか? 「ドメイン」とは正確には何ですか?また、マッピング関数をどのように構築しますか?

例として、「do X while Y」のマッピング関数は何でしょうか?

オンラインでたくさんの資料を読んできましたが、理解するのは難しいです。これらの記述は文脈自由文法に似ているでしょうか?

教えてください、ありがとう！

タイプチェッカーで、特定の計算が終了することが保証されているかどうかを指定できる関数型言語はありますか? あるいは、Haskellだけでこれを行うことはできますか?

Haskellに関して、この回答では、ポスターは次のように述べています

これについての通常の考え方は、すべての Haskell 型が「リフト」されているというものです。これには ⊥ が含まれています。つまり、 だけではなくにBool対応します。これは、Haskell プログラムが終了することが保証されておらず、例外が発生する可能性があるという事実を表しています。{⊥, True, False}{True, False}

一方、アグダに関するこの論文は、次のように述べています。

正しい Agda プログラムとは、型チェックと終了チェックの両方に合格するプログラムです。

つまり、すべての Agda プログラムが終了し、BoolAgda の a は正確に に対応します{True, False}。

たとえば、Haskell では type の値を持つことができますIO a。これは、問題の値を計算するために IO が必要であることをタイプチェッカーに伝えます。Lifted a問題の計算が終了しない可能性があると主張する型を用意できますか? つまり、非終了を許可しますが、型システムで分離します。(明らかに、Agda のように、値を「確実に終了する」と「終了しない可能性がある」にのみ分けることができます) そうでない場合、これを行う言語はありますか?

Haskell でプログラムを作成して、整数変数、1 次元 (整数) 配列、および関数を使用して命令型言語プログラムの表示セマンティクスを計算しようとしています。私が始めている関数は次のタイプです：

State は次のとおりです。

最初の部分は整数変数の値で、2 番目の部分は特定のインデックスにある配列変数の値です。

プログラムには次のような特徴があります。

• progsem は、プログラムの実行後に結果の状態を返します

• 関数には、整数変数用と配列変数用の 2 つのパラメーター リストがあります。

• 関数は値の結果によって呼び出されます

命令型言語の抽象構文は次のとおりです。

さて、具体的な質問はありませんが、セマンティクスの書き方について誰かが私を正しい方向に向けることができるかどうか疑問に思っていました.

過去に、配列と関数を使用しない命令型プログラミング言語に対して同様のことを行いました。それは次のように見えました：

州がそのタイプだった場所

私が言ったように、詳細な回答は必要ありませんが、ヘルプ/ヒント/ポインターは大歓迎です。

私はHaskellウィキブックの表示セマンティクスに関するセクションに取り組んでいますが、この演習でちょっと立ち往生しています:

から始まる不動点の反復によって得られる不動点も最小であり、他のどの不動点よりも小さいことを証明してください。(ヒント:は cpo の最小要素であり、g はモノトーンです)。

次のステートメントは、演習に至るまでの概念の核心を定義しています (私は思います):

ここで、f は階乗関数であり、g が連続であるとすると、g の固定小数点として示されます。

g(f) = f が示されている部分は基本的に理解していると思いますが、演習をどうすればよいかはよくわかりません。私が理解していることから、階乗関数 f は最小不動点 (演算子に基づいて最小) ですが、関数を と比較することが (直感的に) 意味することはまったく明確ではありません。例に示されている最小不動点以外。

g(x) は単調であるため、一方が他方よりも小さい 2 つのものに適用すると、結果は依然としてこの順序に従うことを理解しています。

関数 f' を取り、 を仮定することから証明を開始すると思います。その場合、g の単調な性質を通じて、 を示すことができます。次に、必然的に g(f') = g(f) または f' = f であることを示すことができれば、証明は完了したと思いますが、それを示す方法がわかりません。

Haskell の, は (一般的に)最初の引数をWHNFに減らし、この動作が GHCi で期待どおりであることを理解しています (と思います)。seq

ただし、のドキュメントでevaluateは、引数を WHNF に減らすとも書かれていますが、実際には引数を完全に通常の形式に減らしているようです。

この（明らかな）不一致を確認できます

と

のドキュメントevaluateが正しい場合、seqとの動作はevaluate同じであるべきではありませんか? ここで(Haskellの初心者として)何が欠けていますか?