Semantic Embedding
投喂可爱 PL 知识 :cheese:
shallow embedding / deep embedding（深层嵌入 / 浅层嵌入）
据该帖某 PL 史学家记载，该术语原始出处为 1992 年发表的 “Experience with embedding hardware description languages in HOL”，其讨论了使用高阶逻辑（higher order logic）表达硬件描述语言（HDL）语义，即语义嵌入（semantic embedding）的不同方法。 此前 Why higher-order logic is a good formalisation for specifying and verifying hardware 已经提出了数字电路的高阶逻辑，
作者声称使用“数学逻辑”（mathematical logic）表述硬件规约对很多硬件设计者是不可接受的（unacceptable），而且不适合作为仿真器和综合器的输入形式。然而此处“数学逻辑”指称并不明确，我翻了参考文献也没看明白 :pouting_cat:
在 34 年后的今天，基于模型检查的合规性检查工具在综合器中已然普及，
Hardware can be directly specifed in the notation of mathematical logic [11, 14, 18], but this form is unacceptable to many designers and is also unsuitable for input to CAD tools such as simulators and circuit synthesizers. The work described here aims to support the use of conventional hardware description languages (HDLs) within a general theorem-proving environment.
There are two approaches to embedding HDLs in logic: (1) Represent the abstract syntax of HDL programs by terms, then define within the logic semantic functions that assign meanings to the programs. (2) Only define semantic operators in the logic and arrange that the user-interface parse input from HDL syntax directly to semantic structures, and also print semantic representations in HDL syntax. These two approaches will be referred to as deep embedding and shallow embedding, respectively.
Thanks - now I know who to blame for such horrible terminology.
:pouting_cat: