【PL理论】(16) 形式化语义:语义树 | <Φ, S> ⇒ M | 形式化语义 | 为什么需要形式化语义 | 事实:部分编程语言的设计者并不会形式化语义

  • 💭 写在前面:本章我们将继续探讨形式化语义,讲解语义树,然后我们将讨论“为什么需要形式化语义”,以及讲述一个比较有趣的事实(大部分编程语言设计者其实并不会形式化语义的定义)。

目录

0x00 语义树(Derivation Tree)

0x01 关于实现语言

0x02 为什么需要形式化语义?

0x03 事实:部分编程语言的设计者并不会形式化语义


0x00 语义树(Derivation Tree)

对于程序 \color{} S,如果存在 \color{}M,使得 \left \langle \phi ,S \right \rangle\Rightarrow M,则其语义被定义 (即成功终止) 。 

  • 这里,符号 \color{}\phi 表示初始内存,是空的。

💭 举个例子:用于程序 x=1; y=x+5 的推导树

x = 1
y = x + 5

0x01 关于实现语言

我们可以实现一个解释器来解释我们迄今设计的语言,我们可以尝试使用 F# 来实现解释器。

例如:语义域 \color{}Val=Z+B 可以实现为:

type Val = Int of int | Boolean of bool

例如:表达式的评估可以实现为:

let rec eval (e: Exp) (m: Mem) : Val = ...

归纳定义 (Inductive definition) 可以通过递归实现。

对于某些程序,语义未定义,例如:

y = x + true   // 无法应用任何规则

这类程序可以认为是运行时错误,在实现中,我们将设计解释器让其抛出异常。

0x02 为什么需要形式化语义?

我们上一章到目前为止,都在谈论 形式化语义(formal semantics)

形式化语义是计算机科学和语言学中的一个重要领域。

它旨在使用形式化的数学工具来准确地描述自然语言或计算机程序的含义。

用形式化方法来定义语言的结构和含义,以及推导出语言表达式的含义和行为。

主要目标就是消除歧义,确保语言或程序的含义在不同环境下的一致性和可预测性。

它通常包括以下几种主要方法:

  • 操作语义(Operational Semantics)
  • 语义动态学(Dynamic Semantics)
  • 语义形式学(Denotational Semantics)
  • 公理化语义(Axiomatic Semantics)

.

❓ 思考:为什么需要形式化语义?

因为需要形式地证明某些有用的属性,比如:

  • 证明类型推断算法的正确性。
  • 证明编译器优化的正确性
  • 证明程序分析算法的正确性。

所有这些都与程序的行为 (语义) 相关,因此,我们首先必须定义这种语义,比如:

  • 要证明优化的正确性,我们首先需要定义两个程序的语义等价

0x03 事实:部分编程语言的设计者并不会形式化语义

UUUUnfortunately!!!非常不幸的是,编程语言的爹爹们通常不会 "规范的" 定义其语义!

例如,C 和 JavaScript 的语义是用自然语言口头描述的。

JavaScript 的语义特别复杂,经常令人难以理解(这样产生了许多有趣的研究)

因此,编程语言研究者首先必须正式定义他们想讨论的语言的语义!

例如,CompCert 的作者首先定义了 C 语言的语义,以便制作一个带有正确性证明的编译器。


📌 [ 笔者 ]   王亦优
📃 [ 更新 ]   2023.6.12
❌ [ 勘误 ]   /* 暂无 */
📜 [ 声明 ]   由于作者水平有限,本文有错误和不准确之处在所难免,本人也很想知道这些错误,恳望读者批评指正!

📜 参考资料 

Microsoft. MSDN(Microsoft Developer Network)[EB/OL]. []. .

本文来自互联网用户投稿,该文观点仅代表作者本人,不代表本站立场。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如若转载,请注明出处:http://www.mzph.cn/web/25649.shtml

如若内容造成侵权/违法违规/事实不符,请联系多彩编程网进行投诉反馈email:809451989@qq.com,一经查实,立即删除!

相关文章

adb shell进入设备后的命令

目录 一、查看删除手机 /data/local/tmp/下的文件 二、设置权限 三、查看手机设备正在运行的服务 四、可能需要的adb 命令 一、查看删除手机 /data/local/tmp/下的文件 可以通过以下命令: adb shell # 进入设备 ls /data/local/tmp/ # 查看文件夹下的内容…

DDMA信号处理以及数据处理的流程---原始数据生成

Hello,大家好,我是Xiaojie,好久不见,欢迎大家能够和Xiaojie一起学习毫米波雷达知识,Xiaojie准备连载一个系列的文章—DDMA信号处理以及数据处理的流程,本系列文章将从目标生成、信号仿真、测距、测速、cfar…

服务部署:Linux系统部署C# .NET项目

1. 安装 .NET SDK 首先,你需要在你的 Linux 系统上安装 .NET SDK。 Ubuntu系统: 下载 Microsoft 包配置文件 wget https://packages.microsoft.com/config/ubuntu/20.04/packages-microsoft-prod.deb -O packages-microsoft-prod.deb 这个命令使用 wge…

大模型日报2024-06-10

大模型日报 2024-06-10 大模型资讯 无需矩阵乘法的语言模型在亿参数规模上表现优异 摘要: 研究表明,无需矩阵乘法的语言模型在亿参数规模上仍能保持顶级性能。这一发现挑战了传统神经网络依赖矩阵乘法的观点,展示了在GPU优化之外的新可能性。 博弈论助力…

MySQL基础---库的操作和表的操作(配着自己的实操图,简单易上手)

绪论​ 勿问成功的秘诀为何,且尽全力做您应该做的事吧。–美华纳;本章是MySQL的第二章,本章主要写道MySQL中库和表的增删查改以及对库和表的备份处理,本章是基于上一章所写若没安装mysql可以查看Linux下搭建mysql软件及登录和基本…

编曲市场行情

编曲市场行情 现在的编曲市场是分层级,金字塔模式的市场,对能力要求很高,也非常卷,也确实能赚钱。 底层编曲人:数量最多,以初学者编曲人居多,大部分是那种自学了一个多月就出来标榜自己 是音…

LabVIEW汽车电机测试系统

1. 背景 随着电动汽车的快速发展,汽车电机作为电动汽车的核心部件,其性能评估变得尤为重要。电机的功率、效率、转速等参数直接影响着电动汽车的性能和续航里程。因此,设计一套全面、准确的汽车电机测试系统对于提高电动汽车的性能和安全性具…

离散数学-万字课堂笔记-期末考试-考研复习-北航离散数学1

第一章 逻辑语言1.1 逻辑运算1.2 命题逻辑合式公式1.3 谓词逻辑合式公式1.4 自然语言命题第二章 命题逻辑语义2.1 命题合式公式语义2.2 推论式与等价式的语义2.3 变换合式公式的语义2.4 命题公式范式2.5 等式演算2.6 完全集第三章 谓词逻辑语义3.1谓词合式公式语义3.2推论关系和…

从渲染管线到着色器Shader实践

浏览器渲染管线原理 浏览器渲染管线是浏览器将HTML、CSS和JavaScript转换为用户可见的网页的过程。这一过程涉及多个步骤,包括解析、布局、绘制和合成等。下面是浏览器渲染管线的详细原理: 解析(Parsing): HTML解析:浏览器下载HTML内容后,首先进行HTML解析,将HTML文本…

GO语言 环境搭建

1. ide GoLand 下载地址 感谢您下载GoLand!

如何提升自己的管理思维?

贯彻组织的核心价值观和文化理念,营造积极正向的工作氛围。通过身体力行,管理者可以影响和带动团队成员,共同营造一个充满活力和凝聚力的工作环境,确保组织文化能够深入人心,成为推动组织前进的强大动力。 总之&#x…

“程序员职业素养全解析:技能、态度与价值观的融合“

文章目录 每日一句正能量前言专业精神专业精神的重要性技术执着追求的故事结论 沟通能力沟通能力的重要性团队合作意识实际工作中的沟通案例结论 持续学习持续学习的重要性学习方法进步经验结论 后记 每日一句正能量 梦不是为想象,而是让我们继续前往。 前言 在数字…

【PowerDesigner】创建和管理CDM之新建实体

目录 🌊1. PowerDesigner简介 🌍1.1 常用模型文件 🌍1.2 PowerDesigner使用环境 🌊2. 创建和管理CDM 🌍​​​​​​2.1 新建CDM 🌍2.2 新建实体 🌊1. PowerDesigner简介 🌍1…

【Linux系统化学习】网络层——IP协议

目录 IP协议 协议头格式 两个问题 网段划分 IP地址的分类 CIDR网段划分(无分类编址) 特殊的IP地址 IP地址的数量限制 私有IP地址和公网IP地址 路由 路由表的查询 IP协议 应用层、运输层上两层协议我们只考虑的是通信的双方对应层,…

操作系统入门系列-MIT6.828(操作系统工程)学习笔记(六)---- 初窥操作系统启动流程(xv6启动)

系列文章目录 操作系统入门系列-MIT6.S081(操作系统)学习笔记(一)---- 操作系统介绍与接口示例 操作系统入门系列-MIT6.828(操作系统工程)学习笔记(二)----课程实验环境搭建&#x…

k8s离线部署Calico网络(2续)

下载离线镜像 百度网盘 链接:https://pan.baidu.com/s/14ReJW-ZyYZFLbwSEBZK6mA?pwdi6ct 提取码:i6ct 1.将离线镜像上传至所有服务器并解压: [rootmaster ~]# tar xf calico.tar.gz [rootmaster ~]# cd calico 2.所有服务器使用for循环导入…

ARM交叉编译

目录 一、介绍 1、本地编译 2、交叉编译 二、交叉工具链 1、概念 2、工具 3、获取方法 三、交叉编译运行程序 1、pc机操作(x86_64) ​2、开发板操作(ARM) 一、介绍 1、本地编译 本地编译是在与目标运行环境相同的机器上…

Java 程序结构 -- Java 语言的变量、方法、运算符与注释

大家好,我是栗筝i,这篇文章是我的 “栗筝i 的 Java 技术栈” 专栏的第 003 篇文章,在 “栗筝i 的 Java 技术栈” 这个专栏中我会持续为大家更新 Java 技术相关全套技术栈内容。专栏的主要目标是已经有一定 Java 开发经验,并希望进…

【数据结构】详解堆排序当中的topk问题(leetcode例题)

文章目录 前言如何理解topk问题代码逻辑代码实现 前言 Leetcode相关题目:215. 数组中的第K个最大元素 如何理解topk问题 **Top K 问题是一个经典的问题,在计算机科学中,它的目标是在一组数据中找到前 K 个最大或最小的元素。**这个问题在许…

Vue3学习记录第三天

Vue3学习记录第三天 背景说明学习记录Vue3中shallowReactive()和shallowRef()Vue3中toRaw()和markRaw()前端...语法Vue3中readonly()和shallowReadonly()函数前端的防抖 背景 之前把Vue2的基础学了, 这个课程的后面有简单介绍Vue3的部分. 学习知识容易忘, 这里仅简答做一个记录…