formal-semantics

3熱度

4回答

想象像 exp(49/200)+(x-49/200) 我想傳遞的功能「roundn」的說法無論操作是不是addtion或減法所以我的表情變得 roundn(exp(roundn(49/200, n)), n) + (x - roundn(49/200, n) 好吧，我要處理的表達式是這樣的： exp(49/200)+exp(49/200)*(x-49/200)+1/2*exp(49/20

12熱度

2回答

指稱語義映射是否可確定？

對於我這個問題表達不好的歉意，我不確定我有沒有適當的詞彙來問它。我已經寫了（最近）一個類似於 ⟦let x = x in x⟧ = ⊥ 但實際上我沒有在這裏明白了什麼棘手的。我可以斷言這個陳述真的是⊥，因爲我知道這是一個非生產性的無限循環。此外，我可以斷言類似於 ⟦let ones = 1:ones in ones⟧ = μ(λx.(1,x)) = (1, (1, (1, ...)))

0熱度

2回答

編程語言中的術語「上下文」以及如何通過加載和更新影響上下文？

在上下文無關和上下文敏感的語言中，上下文的含義是什麼？變量是否可以有多個上下文？如果我需要在特定的內存地址中存儲特定的值，那麼會如何影響內存地址的上下文？如果我想更新變量，變量的上下文如何改變？

12熱度

1回答

PLT Redex：參數化語言定義

這是一個嘮叨我一段時間的問題，我想知道這裏有沒有人可以幫忙。我有一種稱爲lambdaLVar的PLT Redex模型，它或多或少是一種花園式的無類型lambda微積分，但擴展了包含「晶格變量」或LVars的存儲。 LVar是一個變量，其值只能隨着時間增加，其中「增加」的含義由語言用戶指定的部分有序集合（又名格）給出。因此lambdaLVar是一個真正的語言家族 - 用一個格子來實例化它，並且你得

5熱度

1回答

CSS盒定位的形式化語義

我是一名（理論）計算機科學專業的學生，因此對編程語言語義的研究是我研究的主題之一（wikipedia）。我玩過很多CSS，對盒子定位規則有合理的理解。（如果您告訴我創建一個具有特定佈局的頁面，我經常會想到正確的方框和適用的CSS規則。）對CSS盒子定位規則有某種形式的語義會很酷，但在搜索了一段時間後，我無法找到任何有用的東西。我大部分只是簡單地結束於CSS規範，它被格式化爲具有僞算法的長

1熱度

1回答

我如何表示這個語法的語義？

我在寫一個語言規範，我需要解決以下基本問題。假設我有（被認爲是人爲的）抽象語法： <A> ::= <B> | <C> <B> ::= 1 | 2 | 3 <C> ::= 4 | 5 | 6 這種語言的指稱語義是什麼樣的？非終端包含在'<'和'>'中，終端不是。我想將1 ... 6映射到自然數域。我不清楚的是我是否需要爲非終端提供映射。似乎我不需要，因爲，例如，<A> ::= <B> | <

3熱度

1回答

什麼是循環不變和最弱的前提

給出一個循環不變，維基百科的名單，一個很好的方式，產生一個循環最弱的先決條件（從http://en.wikipedia.org/wiki/Predicate_transformer_semantics）之間的關係： wp(while E inv I do S, R) = I \wedge \forall y. ((E \wedge I) \implies wp(S,I \we

1熱度

1回答

如何定義表達式翻譯器？

我定義2種幾乎相同的語言（foo和bar）： theory SimpTr imports Main begin type_synonym vname = "string" type_synonym 'a env = "vname ⇒ 'a option" datatype foo_exp = FooBConst bool | FooIConst int |