linda1729
  Post Categories
Beyond Code 9 Blogsmith Notes 2 Computer Networks 7 Course Capsules 4 Database Systems 18 Deep Learning Essentials 12 Formal Semantics 15 Maker’s Notes 8 Studio Works 4 Computer System Engineering 18
等价性证明练习 等价性证明练习
等价性证明练习在形式语义学的研究中，证明两个程序片段在语义上等价（$c_1 \sim c_2$）是一项基础工作。这意味着对于任何初始状态 $\sigma$ 和结束状态 $\sigma’$，$\langle c_1, \sigma \rang
2026-02-03 Formal Semantics
形式语义 等价性证明
小步语义格局变换练习 小步语义格局变换练习
小步语义格局变换练习在小步语义中，我们关注程序执行的每一步演化。一个格局通常表示为 $\langle c, \sigma \rangle$（命令与状态对）或直接是一个状态 $\sigma$（在非变种语义中表示终止）。 以下是针对不同表达式和
2026-02-02 Formal Semantics
形式语义 小步语义
大步语义推导树练习 大步语义推导树练习
大步语义推导树练习大步语义描述了表达式或命令如何直接计算出最终结果或最终状态。推导树则通过逻辑规则的嵌套，清晰地展示了这一演化过程。 题目 1：算术表达式 Aexp题目：在状态 $\sigma = \sigma_{init}[4
2026-02-01 Formal Semantics
形式语义 大步语义
Rocq知识点 Rocq知识点
Rocq知识点一、 常用命令 (Commands) 命令 详细功能说明 举例与输出 Check 查看类型。只进行类型推导，不执行计算。 Check S O. 输出：S O : nat Compute 计算/约化。将表
2026-01-31 Formal Semantics
形式语义 rocq/coq
Rcoq模拟题 Rcoq模拟题
Rcoq模拟题组1一、 系统指令Q1. 在 Rocq 中，命令 Check (negb true). 的主要作用是？A. 计算出该表达式的结果为 false。B. 查看该表达式的类型，结果显示为 bool。C. 检查 negb 这个函数是否
2026-01-30 Formal Semantics
形式语义 rocq/coq
Lambda 演算归约练习 Lambda 演算归约练习
Lambda 演算归约练习Lambda 演算是函数式编程和形式语义学的基础。在进行归约时，理解自由变量捕获、$\alpha$-变换以及归约顺序至关重要。以下是 8 道典型的 Lambda 演算练习题及其详细推导过程。 1. 自由变量捕获与
2026-01-29 Formal Semantics
形式语义 lambda
ch9 lambda演算 ch9 lambda演算
ch9 lambda演算 emmm就是教你lambda演算…… 👉 点击这里阅读下一篇：《Lambda 演算归约练习》
2026-01-28 Formal Semantics
形式语义 lambda
ch8 公理语义 ch8 公理语义
ch8 公理语义 这部分的重点就是霍尔证明，多练练就好啦～ 👉 点击这里阅读下一篇：《ch9 lambda演算》
2026-01-27 Formal Semantics
形式语义 公理语义
ch7 指称语义 ch7 指称语义
ch7 指称语义 是最严格的语义，建立在数学基础上。它的规则是由前面的证明法组合严格证明的，这里只整理了考试的核心部分。 👉 点击这里阅读下一篇：《ch8 公理语义》
2026-01-26 Formal Semantics
形式语义 指称语义
ch6 归纳定义 ch6 归纳定义
ch6 归纳定义 主要在介绍规则归纳法和特殊的规则归纳法，还引入了算子等概念，主要是在为后面指称语义做准备。 👉 点击这里阅读下一篇：《ch7 指称语义》
2026-01-25 Formal Semantics
形式语义 归纳定义
ch5 归纳原理 ch5 归纳原理
归纳原理 各种归纳方法，很有意思，在后续的语义证明中都会用到。 👉 点击这里阅读下一篇：《ch6 归纳定义》
2026-01-24 Formal Semantics
形式语义 归纳原理
ch4 操作语义 ch4 操作语义
ch4 操作语义 最核心的部分啦！其实就是抽象出一种机器，它执行命令的过程为一种语义，再去证明程序的正确性。分为大部语义、小步语义与它们的扩展。 👉 点击这里阅读下一篇：《ch5 归纳原理》
2026-01-23 Formal Semantics
形式语义 操作语义
1 / 2
评论