問題タブ [formal-semantics]

私は非常にばかげた論文を読んでいて、Giottoが「正式なセマンティクス」をどのように定義しているかについて話し続けています。

Giottoには、モードスイッチ、タスク間通信、およびプログラム環境との通信の意味を指定する正式なセマンティクスがあります。

私は限界に達していますが、「正式なセマンティクス」が何を意味するのかを完全に理解することはできません。

多くのプログラミング言語は、一般的でかなり普遍的な機能を共有しています。たとえば、Java、VB6、.NET、PHP、Python を比較すると、制御構造、数値および文字列操作などの共通の関数が見つかります。

これらの機能をメタ言語 (または言語にとらわれない) レベルで定義するために何が行われましたか?

UML はあらゆる面でソフトウェアの説明的な参照を提供しますが、実際の焦点はデータ プロセスにあるようです。UML は関連していますか?

私は、「現在の過多に取って代わる単一の言語がないのはなぜですか」と尋ねているのではありません。私たちは多くの異なるツールを必要としています (少なくともこの時代では)。

私は、すべての言語がテンプレートに適合することを求めているわけではありません -- アセンブリ言語とコンパイル済み言語は、それを実行不可能にするほど十分に異なります (HTML を言語と呼ぶ人もいますが、私はそうは思いません)。どのような試みも、適切に狭い範囲から開始されます。これに沿って、私はモデルが完全な妥当性を持った小さな選択でさえもカバーするとは思わない.

ただし、そのようなモデルを使用して、ある言語から別の言語に転置できると期待しています (目的は限られていますが、一般的な翻訳を考えてください)。

私は (理論的な) コンピューター サイエンスの学生であり、プログラミング言語のセマンティクスの調査は私の研究対象の 1 つです ( wikipedia )。

私は CSS をいろいろいじり、ボックスの配置規則をある程度理解しています。(特定のレイアウトでページを作成するように言われると、正しいボックス アプローチと適用可能な CSS ルールを思いつくことがよくあります。)

CSS のボックスの配置規則にある種の正式なセマンティクスがあればいいのですが、しばらくネットを検索した後も、役立つものはまったく見つかりませんでした。

ほとんどの場合、最終的に CSS 仕様にたどり着きます。これは、疑似アルゴリズムを使用した長いテキストとしてフォーマットされています (最大の読み物ではありません --- これらの仕様は、まだ多くの努力を払って読んでいません)。

この「理論」を、仕様が提供するものよりも厳密な数学的モデルに形式化しようとした人はいませんか? 私は完全なものや決定的なものを探しているわけではありませんが、少なくともボックスを配置する方法が正式な方法でモデル化できれば、それは確かに素晴らしい (そして便利です!) でしょう。

そのような研究を知っている人はいますか？

私はすでに遭遇したトークンのセットを含む環境を持っています。新しいトークンを見るとき、そのトークンを現在の環境に追加したいと思います。基本的には、構文解析を実行する環境での集合和集合演算を表現したいと思います。

Γ'={Γ、x}のようなもの

変数'x'を削除したい場合（環境からxを削除します）

x∈Γの場合、Γ'=Γ--x。

これらの2つの形式を書くための適切な方法は何ですか。ありがとう。

これは私がしばらく悩まされてきた問題であり、ここにいる誰かが助けてくれるのではないかと思います.

私は lambdaLVar と呼ばれる言語の PLT Redex モデルを持っています。これは、多かれ少なかれさまざまな型付けされていないラムダ計算ですが、「格子変数」または LVars を含むストアで拡張されています。LVar は、時間の経過とともに値が増加する変数です。「増加」の意味は、言語のユーザーが指定する部分的に順序付けられたセット (ラティスとも呼ばれます) によって与えられます。したがって、lambdaLVar は実際には言語のファミリーです。1 つのラティスでインスタンス化すると、1 つの言語が得られます。別のラティスを使用すると、別のラティスが得られます。ここでコードを見ることができます。重要なものはlambdaLVar.rktにあります。

lambdaLVar の紙上の定義では、言語定義はユーザー指定のラティスによってパラメーター化されます。長い間、Redex モデルで同じ種類のパラメーター化を行いたいと思っていましたが、これまでのところ、その方法を理解できていません。問題の一部は、言語の文法がユーザーがラティスをインスタンス化する方法に依存することです。ラティスの要素は文法の端子になります。ラティス上で抽象的な文法を Redex で表現する方法がわかりません。

その間、lambdaLVar.rkt をできるだけモジュール化しようとしました。そのファイルで定義されている言語は、特定のラティスに特化されています。つまりmax、最小上限 (lub) 操作としての自然数です。(または、同じように、自然数は によって並べられ<=ます。これは非常に退屈なラティスです。) そのラティスに固有のコードの部分は(define lub-op max)、上部近くの行でありnatural、文法に表示されます。(lubユーザー指定の関数に関して定義されたメタ関数がありlub-opます。後者は単なる Racket 関数であるため、Racketlubにエスケープして を呼び出す必要がありますlub-op。)

lambdaLVar をラティスの選択よりも抽象的な方法で実際に指定する機能を除けば、ラティスの最も必要最小限の要素 (Bot 要素と Top 要素のみ) を使用して lambdaLVar のバージョンを記述できるようにする必要があるように思われます。 Bot <= Top -- そして、define-extended-languageさらに何かを追加するために使用します。たとえば、私が説明した自然格子に特化した lambdaLVar-nats という言語を定義できます。

次に、 lambdaLVarの 2 つのリダクション関係を置き換えるためにslow-rr、いくつかのラッパーを定義できます。fast-rr

ドキュメントからの私の理解では、とextend-reduction-relationのルールを再解釈する必要がありますが、lambdaLVar-nats を使用します。これらすべてをまとめて、新しく拡張されたリダクション関係の 1 つを使用して、私が持っていたテスト スイートを実行してみました。slow-rrfast-rr

最初に受け取ったのは、契約違反の苦情です: small-step-base: input (((l 3)) new) at position 1 does not match its contract. small-step-base のコントラクト ラインは just#:contract (small-step-base Config Config)です。ここで、Configは lambdaLVar-nats の下で再解釈した場合に、lambdaLVar の下で行ったよりも新しい意味を持つ文法の非終端記号です。small-step-base実験として、とのコントラクトを削除しましたsmall-step-slow。

その後、実際に 19 個のテスト プログラムを実行できましたが、そのうちの 10 個は失敗しました。当然のことかもしれませんが、失敗するのはすべて、何らかの方法で自然数の値を持つ LVar を使用するプログラムです。(残りは、LVar のストアとまったく対話しない「純粋な」プログラムです。) したがって、失敗するテストは、まさに拡張文法を使用するものです。

そこで、私はうさぎの穴をたどり続けました。Redex は、既存のすべての判断フォームとメタ関数を、lambdaLVar ではなく lambdaLVar-nats に関連付けるように拡張することを望んでいるようです。それは理にかなっており、私が知る限り、判断フォームでは問題ないように見えますが、メタ関数では問題が発生します。新しいメタ関数で同じ名前の古いメタ関数をオーバーロードしたい (既存の判断フォームがそれを使用しているため) ）そして、それを行う方法はないようです。メタ関数の名前を変更しなければならない場合、それは目的を無効にします。とにかく、まったく新しい判断フォームを作成する必要があるからです。私が望むのは、一種のメタ関数呼び出しの遅延バインディングだと思います!

一言で言えば、私の質問: Redex で、言語の定義を希望どおりにパラメータ化する方法、または言語の定義を希望どおりに拡張する方法はありますか? Redex 生成マクロを作成するだけで済むのでしょうか?

読んでくれてありがとう！

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

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

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

[[1]] =1

[[2]] =2

[[3]] =三

[[4]] =四

[[5]] =五

[[6]] =六

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

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

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

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

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