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 |