问题标签 [formal-semantics]

我正在阅读一篇非常愚蠢的论文，它一直在谈论乔托如何定义“形式语义”。

Giotto 有一个正式的语义，它指定了模式切换、任务间通信以及与程序环境通信的含义。

我处于边缘，但无法完全理解“形式语义”的含义。

许多编程语言共享通用甚至相当普遍的特性。例如，如果您比较 Java、VB6、.NET、PHP、Python，那么您会发现常见的功能，如控制结构、数字和字符串操作等。

为在元语言（或与语言无关）级别定义这些特性做了哪些工作？

UML 在各个方面都提供了软件的描述性参考，但现实世界的焦点似乎是数据处理。UML 是否相关？

我不是在问“为什么我们没有一种单一的语言来取代当前的过多语言。” 我们需要许多不同的工具（至少在这个 eo​​n 中）。

我并不是要求所有语言都适合模板——汇编语言与编译语言的差异足以使这不可行（有些人称 HTML 为一种语言，尽管我不会）。任何尝试都将从适当狭窄的范围开始。与此一致，我不希望该模型涵盖即使是一小部分具有完全有效性的选择。

然而，我希望这样的模型可以用于从一种语言转换为另一种语言（目标有限——想想 jist 翻译）。

我是一名（理论）计算机科学专业的学生，​​因此研究编程语言的语义是我研究的主题之一（维基百科）。

我玩过很多 CSS 并且对盒子的定位规则有一个合理的理解。（如果你告诉我创建一个具有特定布局的页面，我通常可以想到正确的框方法和适用的 CSS 规则。）

为 CSS 框定位规则提供某种形式的语义会很酷，但是在网上搜索了一段时间后，我找不到任何有用的东西。

我大多只是简单地以 CSS 规范结束，这些规范被格式化为带有伪算法的长文本（不是最好的阅读材料——我还没有花太多精力阅读这些规范中的任何一个）。

没有人试图将这个“理论”形式化为某种数学模型，比规范所提供的更严格吗？我不是在寻找完整或确定的东西，但如果至少可以以正式的方式对盒子的放置方式进行建模，那么它肯定会很整洁（而且很有用！）。

有人知道这样的研究吗？

我有一个环境，其中包含一组我已经遇到过的令牌；当我查看一个新令牌时，我想将该令牌添加到当前环境中。基本上我想在我执行解析的环境上表达一个集合联合操作。

像Γ' = {Γ, x}

如果我想删除变量“x”（从环境中删除 x）

Γ' = Γ - x 如果 x ∈ Γ 。

写这两种形式的正确方法是什么。谢谢。

这是一个困扰我一段时间的问题，我想知道这里是否有人可以提供帮助。

我有一个名为 lambdaLVar 的语言的 PLT Redex 模型，它或多或少是一种普通的无类型 lambda 演算，但扩展了包含“晶格变量”或 LVars 的存储。LVar 是一个变量，其值只能随时间增加，其中“增加”的含义由语言用户指定的部分有序集合（又名格）给出。因此 lambdaLVar 实际上是一个语言家族——用一个格子实例化它，你就会得到一种语言；用不同的格子，你得到另一个。你可以看看这里的代码；重要的东西在lambdaLVar.rkt中。

在 lambdaLVar 的纸上定义中，语言定义由用户指定的格参数化。很长一段时间以来，我都想在 Redex 模型中做同样的参数化，但到目前为止，我还没有弄清楚如何做。部分麻烦在于语言的语法取决于用户如何实例化格：格的元素成为语法中的终结符。我不知道如何在 Redex 中表达一个在格上抽象的语法。

同时，我尝试使 lambdaLVar.rkt 尽可能模块化。该文件中定义的语言专门用于特定的格：自然数max作为最小上界（lub）操作。（或者，等效地，按 . 排序的自然数<=。这是一个非常无聊的格子。）特定于该格子的代码的唯一部分是(define lub-op max)靠近顶部的行，并natural出现在语法中。（有一个lub根据用户指定的函数定义的元lub-op函数。后者只是一个 Racket 函数，因此lub必须转义到 Racket 才能调用lub-op。）

除非能够以一种对晶格选择抽象的方式实际指定 lambdaLVar，否则我似乎应该能够编写一个具有最简单晶格的 lambdaLVar 版本——只有 Bot 和 Top 元素，其中Bot <= Top -- 然后define-extended-language用来添加更多东西。例如，我可以定义一种名为 lambdaLVar-nats 的语言，它专门用于我描述的 naturals lattice：

然后，为了替换两个归约关系slow-rr以及fast-rr我为 lambdaLVar 所拥有的关系，我可以定义几个包装器：

我对文档的理解extend-reduction-relation是，它应该重新解释 and 中的规则slow-rr，fast-rr但使用 lambdaLVar-nats。将所有这些放在一起，我尝试使用新的扩展缩减关系之一运行我拥有的测试套件：

我收到的第一件事是违反合同的投诉：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-nats 而不是 lambdaLVar 相关联。这是有道理的，据我所知，它似乎对判断形式有效，但是对于元函数我遇到了麻烦：我希望新的元函数重载同名的旧元函数（因为现有的判断形式正在使用它) 并且似乎没有办法做到这一点。如果我必须重命名元函数，那就达不到目的了，因为无论如何我都必须编写全新的判断形式。我想我想要的是一种元函数调用的后期绑定！

简而言之，我的问题是： Redex 中是否有任何方法可以以我想要的方式参数化语言的定义，或者以某种方式扩展语言的定义，从而满足我的需求？我最终只需要编写生成 Redex 的宏吗？

谢谢阅读！

我正在编写语言规范，我需要解决以下基本问题。假设我有（诚然做作的）抽象语法：

这种语言的指称语义是什么样的？非终结符包含在 '<' 和 '>' 中，终结符不是。我想将1...映射6到自然数域。我完全不清楚的是我是否需要为非终端提供映射。似乎我不需要，因为，例如，<A> ::= <B> | <C>没有意义；它只是一个结构。忽略，暂时我们可以完全消除这条规则。

所以，就目前而言，这就是我认为完整的指称定义应该是这样的，其中右侧（斜体）表示自然数的相应值：

[[1]] =一

[[2]] =二

[[3]] =三

[[4]] =四

[[5]] =五

[[6]] =六

A从美学上讲，不提,B或根本不提似乎很奇怪C，但我认为这些符号永远不会出现在实际程序中（如4：），所以也许这就足够了。我所拥有的关于这个主题的所有材料都在他们的讨论中忽略了语言定义过程的这个非常简单的具体细节。

我对指称语义的概念有点困惑。据我了解，指称语义应该描述函数和表达式在特定编程语言中的工作方式。用于描述这些功能以及它们如何工作的正确形式究竟是什么？“域”到底是什么，如何构建映射功能？

例如，“do X while Y”的映射函数是什么？

我一直在网上阅读很多资料，但很难理解。这些描述会类似于上下文无关语法吗？

请告诉我，谢谢！

我的任务是学习PHP，但有很多东西我不明白。例如，“变量函数”的概念不是我在其他任何地方看到的。还有许多其他示例，但为简洁起见，我找到了 PHPWTF，其中包含许多 PHP 特质的示例。

我使用过的大多数其他语言要么有正式规范（例如，Haskell 2010），要么至少有一篇关于其形式语义的研究论文（例如，用于 Javascript 的 this）。但是，我找不到任何可与 PHP 相媲美的东西。

有一个官方的“语言参考”。但是，它非常不正式，读起来像 wiki，并且缺少整个部分（例如，语法部分根本没有定义语法）。证实了我的怀疑，这家伙告诉我没有官方规范，甚至没有定义的语法。

维基百科有一篇关于“PHP 语法和语义”的文章，但它只涉及语法，几乎没有提到语义。

我在 PHP 上找到的一篇论文是这篇关于其赋值语义的论文。这是该语言的一个非常小的片段，如果没有一些上下文，可能对我没有多大用处。还有一篇关于 'SaferPHP' 的论文，它可能必须与 PHP 的某些定义一起使用，尽管我看不到任何内容。

解释器/编译器提供语义，所以我想看看这些。然而，Zend 源代码令人生畏（尽管它确实提供了有用的测试用例），HipHop 运行到 270 万个 LoC。（我发现人们投入巨大的精力为一种语言编写编译器而从未编写过规范之类的东西，这让我感到惊讶。）

我想看看 PHP 的类型系统以获得指导，就像 TypeScript 为 JavaScript 提供一些指导一样。我在 Hack 上发现了这些诱人的幻灯片，Hack是 PHP 的一个可选类型系统。然而，这只是幻灯片，目前该项目似乎是 Facebook 的内部项目。

有没有人知道比这些穷人的语义更好的东西？还是每个人都只是“以身作则”？

我想知道语义和概念之间有什么区别？一种语言是否有可能显示概念但不显示语义？是否可以使用语言语法对概念进行建模？剂量UML显示系统的竞争和语义？谢谢 id 提前