标签: formal-semantics

我正在学习/试验Rust,在我用这种语言找到的所有优雅中,有一个让我感到困惑并且看起来完全不合适的特点.

在进行方法调用时,Rust会自动取消引用指针.我做了一些测试来确定确切的行为:

struct X { val: i32 }
impl std::ops::Deref for X {
    type Target = i32;
    fn deref(&self) -> &i32 { &self.val }
}

trait M { fn m(self); }
impl M for i32   { fn m(self) { println!("i32::m()");  } }
impl M for X     { fn m(self) { println!("X::m()");    } }
impl M for &X    { fn m(self) { println!("&X::m()");   } }
impl M for &&X   { fn m(self) { println!("&&X::m()");  } }
impl M for &&&X  { …

我知道的比任何其他语言都要多,每次我需要一些小东西时,我都会通过谷歌搜索"Bash".因此,我可以拼凑出似乎有用的小脚本.不过,我并不真正知道发生了什么事情,我希望的是更正式的介绍bash作为编程语言.例如:评估顺序是什么？范围规则是什么？什么是打字规则,例如一切都是字符串？程序的状态是什么 - 它是字符串到变量名的键值赋值; 还有更多,例如堆栈？有堆吗？等等.

我想咨询GNU Bash手册以获得这种洞察力,但它似乎并不是我想要的; 它更像是句法糖的清单,而不是核心语义模型的解释.在线的百万个"bash教程"只会更糟.也许我应该先学习sh,并将Bash理解为一种语法糖？不过,我不知道这是否是一个准确的模型.

有什么建议？

编辑:我被要求提供一些理想我正在寻找的例子.我认为"形式语义"的一个相当极端的例子是本文关于"JavaScript的本质".也许一个稍微不那么正式的例子是Haskell 2010报告.

我试图通过阅读原始规范来围绕ES6中新的标准化块级功能.我的肤浅理解是:

• ES6中允许块级函数声明.
• 他们升到了街区的顶部.
• 在严格模式下,它们在包含块外部不可见.

然而,由于这些语义的一部分被指定为"可选的"并且仅对于Web浏览器是必需的(附件B),因此这进一步复杂化.所以我想填写下表:

                                             |  Visible outside of block?  |  Hoisted? Up to which point?  |   "TDZ"? |
------------------------------------------------------------------------------------------------------------------------
|   Non-strict mode,   no "web extensions"   |                             |                               |          |
|   Strict mode,       no "web extensions"   |                             |                               |          |
|   Non strict mode,   with "web extensions  |                             |                               |          |
|   Strict mode,       with "web extensions" |                             |                               |          |

另外我不清楚在这种情况下"严格模式"是什么意思.这种区别似乎在附件B3.3中引入,作为函数声明的运行时执行的一些附加步骤的一部分:

1. If strict is false, then
...

但是,据我所知,strict指[[Strict]]的是函数对象的内部插槽.这是否意味着:

// Non-strict …

对于我对这个问题的不良表达表示歉意,我不确定我是否有适当的词汇量.

我写了(最近)类似的东西

?let x = x in x? = ?

但是我真的没有理解这里棘手的事情.我可以断言这句话是真的,? 因为我知道这是一个非生产性的无限循环.此外,我可以断言像

?let ones = 1:ones in ones? = ?(?x.(1,x)) = (1, (1, (1, ... )))

但是什么进入了省略？据推测,它是无限数量的"一元组",如果你对AFA没问题,这是一个非常明确的数学对象,但我怎么能说服你,它不是一些有限数量的"一元组"然后是非生产性的?？

显然,这涉及到解决停止问题,所以我不能一般.

那么在这种情况下,我们如何计算语义映射,就像它们是一个完整的函数一样？对于图灵不完整的语言,语义必然是不确定的吗？我想这意味着语义总是只是一种语言的近似,非正式的描述,但这个"洞"是否会更进一步？

这是一个一直困扰着我的问题,我想知道这里是否有人可以提供帮助.

我有一个名为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的语言,它专门用于我描述的自然格点:

;; Grammar for elements of a lattice of natural numbers.
(define-extended-language lambdaLVar-nats
  lambdaLVar
  (StoreVal .... ;; Extend the original language
            natural))

;; All we have to specify is the lub operation; leq is implicitly <=
(define-metafunction/extension lub lambdaLVar-nats …

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

举个例子,"做Y同时Y"的映射函数是什么？

我一直在网上阅读大量资料,但这很难理解.这些描述是否类似于无上下文语法？

请让我知道,谢谢!

有人告诉我 Rust 在仿射逻辑中具有语义——所以有删除/弱化但没有重复/收缩。

编译如下：

fn throw_away<A, B>(x: A, _y: B) -> A {
    x
}

由于不允许重复，因此无法编译以下内容：

fn dup<A>(x: A) -> (A, A) {
    (x, x)
}

同样，这些都不编译：

fn throw_away3<A, B>(x: A, f: fn(A) -> B) -> A {
    x;
    f(x)
}

fn throw_away4<A, B>(x: A, f: fn(A) -> B) -> A {
    throw_away(x, f(x))
}

弱化也是有目共睹的

fn weaken<A, B, C>(f: fn(A) -> B) -> impl Fn(A, C) -> B {
    move |x: A, y: C| f(x)
}

fn(A, C) -> …

编辑

考虑以下关于参考ECMAScript语言规范的答案响应- 11.13.2化合物分配

考虑为什么这些,

javascript:
   o="";  o = o + (o+=1)    ; alert(o);
   o="";  o =     (o+=1) + o; alert(o);

不一样.从左到右的脚本评估存在时间语义问题(参考:ECMA规范. - 加法运算符).一个结果是+操作员不一定是可交换的.

这可以通过以下方式看出:

javascript:
   o=1;  o = o + (o+=1)    ; alert(o);
   o=1;  o =     (o+=1) + o; alert(o);

要么

javascript:
   o=" _ ";  o = o + (o+=1)    ; alert(o);
   o=" _ ";  o =     (o+=1) + o; alert(o);

懒惰的评估范例,由我错误地和不恰当地使用从而产生下面的问题,也是我个人工作方式的一个不好的属性.

原帖

以下考虑因素可能已经得到解决,但似乎没有.如果是这样,是否可以提供与讨论的链接？

Gecko Javascript运行时引擎的正式指称语义是一个谜.经验测试令人筋疲力尽,无法详尽无遗.

• 是否有可用的权威形式规范或官方参考,明确定义Gecko如何解释Javascript？

参考文献ECMAScript语言规范似乎不够,但是为这些脚本的混合提供了信任,例如, …

我正在阅读一篇非常愚蠢的论文,并继续谈论乔托如何定义"形式语义".

Giotto具有正式的语义,指定模式切换,任务间通信以及与程序环境通信的含义.

我处于边缘,但却无法完全理解"形式语义"的含义.

我的任务是学习PHP,但有很多事情我不明白.例如,"变量函数"的概念不是我在其他任何地方看到过的.还有很多其他的例子,但为了简洁起见,我发现了PHPWTF,它有许多PHP特性的例子.

我使用的大多数其他语言都有正式规范(例如,Haskell 2010)或至少有关于其形式语义的研究论文(例如,这适用于Javascript).但是,我找不到任何可比的PHP.

有一个官方的"语言参考".但是,它非常非正式,读起来像一个维基,并且缺少整个部分(例如,关于语法的部分根本没有定义语法).确认我怀疑的是,这个人告诉我没有正式的规范,甚至没有定义的语法.

维基百科有一篇关于"PHP语法和语义"的文章,但它只涉及语法,几乎没有提到语义.

我在PHP 上发现的一篇论文是关于它的赋值语义的论文.这是该语言的一个非常小的片段,如果没有某些语境,可能对我没什么用处.还有关于'SaferPHP'的论文,它可能与PHP的一些定义有关,虽然我看不到任何.

口译员/编译器提供语义,所以我想看看这些.然而,Zend源是令人生畏的(虽然它确实提供了有用的测试用例),而HipHop则运行到270万LoC.(我发现人们为编写一种语言的编译器付出了巨大的努力而没有编写类似规范的东西.)

我想过为PHP寻找类型系统的指导,就像TypeScript为JavaScript提供一些指导一样.我在Hack上发现了这些诱人的幻灯片,Hack是PHP的可选类型系统.然而,它只是幻灯片,而且此时项目似乎是Facebook的内部项目.

有谁知道比这些穷人的语义更好的东西？或者每个人都只是"通过实例学习"？