class Number < Struct.new(:value)
def to_s
value.to_s
end
def inspect
"<<#{self}>>"
end
end
class Add < Struct.new(:left,:right)
def to_s
"(#{left} + #{right})"
end
def inspect
"<<#{self}>>"
end
end
class Minus < Struct.new(:left,:right)
def to_s
"(#{left} - #{right})"
end
def inspect
"<<#{self}>>"
end
end
class Multiply < Struct.new(:left,:right)
def to_s
"(#{left} * #{right})"
end
def inspect
"<<#{self}>>"
end
end
class Divide < Struct.new(:left,:right)
def to_s
"(#{left} / #{right})"
end
def inspect
"<<#{self}>>"
end
end
class Number < Struct.new(:value)
def to_s
value.to_s
end
def reducible?
false
end
def inspect
"<<#{self}>>"
end
end
class Add < Struct.new(:left,:right)
def to_s
"(#{left} + #{right})"
end
def reducible?
true
end
def reduce
if left.reducible?
Add.new(left.reduce,right)
elsif right.reducible?
Add.new(left,right.reduce)
else
Number.new(left.value + right.value)
end
end
def inspect
"<<#{self}>>"
end
end
class Minus < Struct.new(:left,:right)
def to_s
"(#{left} - #{right})"
end
def reducible?
true
end
def reduce
if left.reducible?
Minus.new(left.reduce,right)
elsif right.reducible?
Minus.new(left,right.reduce)
else
Number.new(left.value - right.value)
end
end
def inspect
"<<#{self}>>"
end
end
class Multiply < Struct.new(:left,:right)
def to_s
"(#{left} * #{right})"
end
def reducible?
true
end
def reduce
if left.reducible?
Multiply.new(left.reduce,right)
elsif right.reducible?
Multiply.new(left,right.reduce)
else
Number.new(left.value * right.value)
end
end
def inspect
"<<#{self}>>"
end
end
class Divide < Struct.new(:left,:right)
def to_s
"(#{left} / #{right})"
end
def reducible?
true
end
def reduce
if left.reducible?
Divide.new(left.reduce,right)
elsif right.reducible?
Divide.new(left,right.reduce)
else
Number.new(left.value / right.value)
end
end
def inspect
"<<#{self}>>"
end
end
class AbstractMachine < Struct.new(:statement)
def step_next
self.statement = statement.reduce
end
def run
while statement.reducible?
puts "#{statement},#{var_enviroment}"
step_next
end
puts "#{statement}" # final state
end
end
class Boolean < Struct.new(:value)
def to_s
value.to_s
end
def inspect
"<<#{self}>>"
end
def reducible?
false
end
end
class LessThan < Struct.new(:left, :right)
def to_s
"#{left} < #{right}"
end
def inspect
"#{self}"
end
def reducible?
true
end
def reduce
if left.reducible?
LessThan.new(left.reduce,right)
elsif right.reducible?
LessThan.new(left,right.reduce)
else
Boolean.new(left.value < right.value)
end
end
end
class GreaterThan < Struct.new(:left, :right)
def to_s
"#{left} > #{right}"
end
def inspect
"#{self}"
end
def reducible?
true
end
def reduce
if left.reducible?
GreaterThan.new(left.reduce,right)
elsif right.reducible?
GreaterThan.new(left,right.reduce)
else
Boolean.new(left.value > right.value)
end
end
end
class Equal < Struct.new(:left, :right)
def to_s
"#{left} == #{right}"
end
def inspect
"#{self}"
end
def reducible?
true
end
def reduce
if left.reducible?
Equal.new(left.reduce,right)
elsif right.reducible?
Equal.new(left,right.reduce)
else
Boolean.new(left.value == right.value)
end
end
end
class LessEqualThan < Struct.new(:left, :right)
def to_s
"#{left} <= #{right}"
end
def inspect
"#{self}"
end
def reducible?
true
end
def reduce
if left.reducible?
LessEqualThan.new(left.reduce,right)
elsif right.reducible?
LessEqualThan.new(left,right.reduce)
else
Boolean.new(left.value <= right.value)
end
end
end
class GreaterEqualThan < Struct.new(:left, :right)
def to_s
"#{left} >= #{right}"
end
def inspect
"#{self}"
end
def reducible?
true
end
def reduce
if left.reducible?
GreaterEqualThan.new(left.reduce,right)
elsif right.reducible?
GreaterEqualThan.new(left,right.reduce)
else
Boolean.new(left.value >= right.value)
end
end
end
class Variable < Struct.new(:name)
def to_s
name.to_s
end
def inspect
"<<#{self}>>"
end
def reducible?
true
end
def reduce(var_enviroment)
var_enviroment[name]
end
end
class Add < Struct.new(:left,:right)
def to_s
"(#{left} + #{right})"
end
def reducible?
true
end
def reduce(var_enviroment)
if left.reducible?
Add.new(left.reduce(var_enviroment),right)
elsif right.reducible?
Add.new(left,right.reduce(var_enviroment))
else
Number.new(left.value + right.value)
end
end
def inspect
"<<#{self}>>"
end
end
class Minus < Struct.new(:left,:right)
def to_s
"(#{left} - #{right})"
end
def reducible?
true
end
def reduce(var_enviroment)
if left.reducible?
Minus.new(left.reduce(var_enviroment),right)
elsif right.reducible?
Minus.new(left,right.reduce(var_enviroment))
else
Number.new(left.value - right.value)
end
end
def inspect
"<<#{self}>>"
end
end
class Multiply < Struct.new(:left,:right)
def to_s
"(#{left} * #{right})"
end
def reducible?
true
end
def reduce(var_enviroment)
if left.reducible?
Multiply.new(left.reduce(var_enviroment),right)
elsif right.reducible?
Multiply.new(left,right.reduce(var_enviroment))
else
Number.new(left.value * right.value)
end
end
def inspect
"<<#{self}>>"
end
end
class Divide < Struct.new(:left,:right)
def to_s
"(#{left} / #{right})"
end
def reducible?
true
end
def reduce(var_enviroment)
if left.reducible?
Divide.new(left.reduce(var_enviroment),right)
elsif right.reducible?
Divide.new(left,right.reduce(var_enviroment))
else
Number.new(left.value / right.value)
end
end
def inspect
"<<#{self}>>"
end
end
class LessThan < Struct.new(:left, :right)
def to_s
"#{left} < #{right}"
end
def inspect
"#{self}"
end
def reducible?
true
end
def reduce(var_enviroment)
if left.reducible?
LessThan.new(left.reduce(var_enviroment),right)
elsif right.reducible?
LessThan.new(left,right.reduce(var_enviroment))
else
Boolean.new(left.value < right.value)
end
end
end
class GreaterThan < Struct.new(:left, :right)
def to_s
"#{left} > #{right}"
end
def inspect
"#{self}"
end
def reducible?
true
end
def reduce(var_enviroment)
if left.reducible?
GreaterThan.new(left.reduce(var_enviroment),right)
elsif right.reducible?
GreaterThan.new(left,right.reduce(var_enviroment))
else
Boolean.new(left.value > right.value)
end
end
end
class Equal < Struct.new(:left, :right)
def to_s
"#{left} == #{right}"
end
def inspect
"#{self}"
end
def reducible?
true
end
def reduce(var_enviroment)
if left.reducible?
Equal.new(left.reduce(var_enviroment),right)
elsif right.reducible?
Equal.new(left,right.reduce(var_enviroment))
else
Boolean.new(left.value == right.value)
end
end
end
class LessEqualThan < Struct.new(:left, :right)
def to_s
"#{left} <= #{right}"
end
def inspect
"#{self}"
end
def reducible?
true
end
def reduce(var_enviroment)
if left.reducible?
LessEqualThan.new(left.reduce(var_enviroment),right)
elsif right.reducible?
LessEqualThan.new(left,right.reduce(var_enviroment))
else
Boolean.new(left.value <= right.value)
end
end
end
class GreaterEqualThan < Struct.new(:left, :right)
def to_s
"#{left} >= #{right}"
end
def inspect
"#{self}"
end
def reducible?
true
end
def reduce(var_enviroment)
if left.reducible?
GreaterEqualThan.new(left.reduce(var_enviroment),right)
elsif right.reducible?
GreaterEqualThan.new(left,right.reduce(var_enviroment))
else
Boolean.new(left.value >= right.value)
end
end
end
虚拟机的类也必须跟着改动:
class AbstractMachine < Struct.new(:statement,:var_enviroment)
def step_next
self.statement, self.var_enviroment = statement.reduce(var_enviroment)
end
def run
while statement.reducible?
puts "#{statement},#{var_enviroment}"
step_next
end
puts "#{statement},#{var_enviroment}" # final state
end
end
下面可以测试变量定义了:
=begin
x <= y + z
4 <= y + z
4 <= 2 + z
4 <= 2 + 8
4 <= 10
true
相当于:
x = 4;
y = 2;
z = 8;
puts x <= y + z;
=> true
=end
AbstractMachine.new(
LessEqualThan.new(
Variable.new(:x),
Add.new(
Variable.new(:y),
Variable.new(:z))),
{x: Number.new(4), y: Number.new(2), z: Number.new(8)}
).run
class DoNothing
def to_s
"do-nothing"
end
def inspect
"#{self}"
end
def ==(other_statement)
other_statement.instance_of?(DoNothing)
end
def reducible?
false
end
end
class Assign < Struct.new(:name,:expression)
def to_s
"#{name} = #{expression}"
end
def inspect
"<<#{self}>>"
end
def reducible?
true
end
def reduce(var_enviroment)
if expression.reducible?
[Assign.new(name,expression.reduce(var_enviroment)), var_enviroment]
else
[DoNothing.new, var_enviroment.merge({name => expression})]
end
end
end
class Number < Struct.new(:value)
def to_s
value.to_s
end
def evaluate(var_eniroment)
self
end
def inspect
"<<#{self}>>"
end
end
class Boolean < Struct.new(:value)
def to_s
value.to_s
end
def evaluate(var_eniroment)
self
end
def inspect
"<<#{self}>>"
end
end
class Add < Struct.new(:left,:right)
def to_s
"(#{left} + #{right})"
end
def inspect
"<<#{self}>>"
end
def evaluate(var_eniroment)
Number.new(left.evaluate(var_eniroment).value + right.evaluate(var_eniroment).value)
end
end
class Minus < Struct.new(:left,:right)
def to_s
"(#{left} - #{right})"
end
def inspect
"<<#{self}>>"
end
def evaluate(var_eniroment)
Number.new(left.evaluate(var_eniroment).value - right.evaluate(var_eniroment).value)
end
end
class Multiply < Struct.new(:left,:right)
def to_s
"(#{left} * #{right})"
end
def inspect
"<<#{self}>>"
end
def evaluate(var_eniroment)
Number.new(left.evaluate(var_eniroment).value * right.evaluate(var_eniroment).value)
end
end
class Divide < Struct.new(:left,:right)
def to_s
"(#{left} / #{right})"
end
def inspect
"<<#{self}>>"
end
def evaluate(var_eniroment)
Number.new(left.evaluate(var_eniroment).value / right.evaluate(var_eniroment).value)
end
end
class LessThan < Struct.new(:left, :right)
def to_s
"#{left} < #{right}"
end
def inspect
"#{self}"
end
def evaluate(var_eniroment)
Boolean.new(left.evaluate(var_eniroment).value < right.evaluate(var_eniroment).value)
end
end
class GreaterThan < Struct.new(:left, :right)
def to_s
"#{left} > #{right}"
end
def inspect
"#{self}"
end
def evaluate(var_eniroment)
Boolean.new(left.evaluate(var_eniroment).value > right.evaluate(var_eniroment).value)
end
end
class Equal < Struct.new(:left, :right)
def to_s
"#{left} == #{right}"
end
def inspect
"#{self}"
end
def evaluate(var_eniroment)
Boolean.new(left.evaluate(var_eniroment).value == right.evaluate(var_eniroment).value)
end
end
class LessEqualThan < Struct.new(:left, :right)
def to_s
"#{left} <= #{right}"
end
def inspect
"#{self}"
end
def evaluate(var_eniroment)
Boolean.new(left.evaluate(var_eniroment).value <= right.evaluate(var_eniroment).value)
end
end
class GreaterEqualThan < Struct.new(:left, :right)
def to_s
"#{left} >= #{right}"
end
def inspect
"#{self}"
end
def evaluate(var_eniroment)
Boolean.new(left.evaluate(var_eniroment).value >= right.evaluate(var_eniroment).value)
end
end
class Assign < Struct.new(:name,:expression)
def to_s
"#{name} = #{expression}"
end
def inspect
"<<#{self}>>"
end
def evaluate(var_eniroment)
var_eniroment.merge({ name => expression.evaluate(var_eniroment)})
end
end
class If < Struct.new(:condition, :true_statement, :false_statement)
def to_s
"if (#{condition}) { #{true_statement} } else { #{false_statement} }"
end
def inspect
"#{self}"
end
def evaluate(var_eniroment)
case condition.evaluate(var_eniroment)
when Boolean.new(true)
true_statement.evaluate(var_eniroment)
when Boolean.new(false)
false_statement.evaluate(var_eniroment)
end
end
end
class DoNothing
def to_s
"do-nothing"
end
def inspect
"#{self}"
end
def ==(other_statement)
other_statement.instance_of?(DoNothing)
end
def evaluate(var_eniroment)
var_eniroment
end
end
# -> e { } 是参数为e的lambda表达式 是Ruby语言的lambda语法
class Number < Struct.new(:value)
def to_ruby
"-> e { #{value.inspect} }"
end
def inspect
"<<#{self}>>"
end
end
class Boolean < Struct.new(:value)
def to_ruby
"-> e { #{value.inspect} }"
end
def inspect
"<<#{self}>>"
end
end
如果在Ruby console上运行以上代码:
# => "-> e { 2 }"
Number.new(2).to_ruby
# => "-> e { true }"
Boolean.new(true).to_ruby
class Variable < Struct.new(:name)
def to_ruby
"-> e { e[#{name.inspect}] }"
end
def inspect
"<<#{self}>>"
end
end
# => "-> e { e[:test] }"
expression = Variable.new(:test)
expression.to_ruby
# => 6
proc = eval(expression.to_ruby)
proc.call({ test: 6})
加减乘除大于小于等操作符:
class Add < Struct.new(:left,:right)
def to_ruby
"-> e { (#{left.to_ruby}).call(e) + (#{right.to_ruby}).call(e) }"
end
def inspect
"<<#{self}>>"
end
end
class Minus < Struct.new(:left,:right)
def to_ruby
"-> e { (#{left.to_ruby}).call(e) - (#{right.to_ruby}).call(e) }"
end
def inspect
"<<#{self}>>"
end
end
class Multiply < Struct.new(:left,:right)
def to_ruby
"-> e { (#{left.to_ruby}).call(e) * (#{right.to_ruby}).call(e) }"
end
def inspect
"<<#{self}>>"
end
end
class Divide < Struct.new(:left,:right)
def to_ruby
"-> e { (#{left.to_ruby}).call(e) / (#{right.to_ruby}).call(e) }"
end
def inspect
"<<#{self}>>"
end
end
class LessThan < Struct.new(:left, :right)
def to_ruby
"-> e { (#{left.to_ruby}).call(e) < (#{right.to_ruby}).call(e) }"
end
def inspect
"#{self}"
end
end
class GreaterThan < Struct.new(:left, :right)
def to_ruby
"-> e { (#{left.to_ruby}).call(e) > (#{right.to_ruby}).call(e) }"
end
def inspect
"#{self}"
end
end
class Equal < Struct.new(:left, :right)
def to_ruby
"-> e { (#{left.to_ruby}).call(e) == (#{right.to_ruby}).call(e) }"
end
def inspect
"#{self}"
end
end
class LessEqualThan < Struct.new(:left, :right)
def to_ruby
"-> e { (#{left.to_ruby}).call(e) <= (#{right.to_ruby}).call(e) }"
end
def inspect
"#{self}"
end
end
class GreaterEqualThan < Struct.new(:left, :right)
def to_ruby
"-> e { (#{left.to_ruby}).call(e) >= (#{right.to_ruby}).call(e) }"
end
def inspect
"#{self}"
end
end
然后对以上代码进行测试:
# "-> e { (-> e { e[:a] }).call(e) + (-> e { 4 }).call(e) }"
Add.new(Variable.new(:a),Number.new(4)).to_ruby
# "-> e { (-> e { (-> e { e[:a] }).call(e) - (-> e { 2 }).call(e) }).call(e) > (-> e { 5 }).call(e) }"
GreaterThan.new(Minus.new(Variable.new(:a),Number.new(2)),Number.new(5)).to_ruby
# => 10
var_environment = { x: 6 }
proc = eval(Add.new(Variable.new(:x),Number.new(4)).to_ruby)
proc.call(var_environment)
# => false
proc = eval(GreaterThan.new(Minus.new(Variable.new(:x),Number.new(2)),Number.new(5)).to_ruby)
proc.call(var_environment)
语句
Assign给变量赋值无非还是修改Hash表上下文环境:
class Assign < Struct.new(:name,:expression)
def to_ruby
"-> e { e.merge({ #{name.inspect} => (#{expression.to_ruby}).call(e) }) }"
end
def inspect
"#{self}"
end
end
# "-> e { e.merge({ :foo => (-> e { (-> e { e[:bar] }).call(e) + (-> e { 2 }).call(e) }).call(e) }) }"
statement = Assign.new(:foo, Add.new(Variable.new(:bar),Number.new(2)))
statement.to_ruby
# => {:bar=>6, :foo=>8}
proc = eval(statement.to_ruby)
proc.call({ bar: 6})
DoNothing啥也不做，一个啥都不做的lambda表达式:
class DoNothing
def to_ruby
"-> e { e }"
end
end
最后程序代码块，逻辑控制if while语句:
class If < Struct.new(:condition, :true_statement, :false_statement)
def to_ruby
"-> e {" +
"if (#{condition.to_ruby}).call(e)" +
"then (#{true_statement.to_ruby}).call(e)" +
"else (#{false_statement.to_ruby}).call(e)" +
"end" +
"}"
end
end
=begin
=> "-> e { if (-> e { true }).call(e)
then (-> e { e.merge({ :foo => (-> e { 3 }).call(e) }) }).call(e)
else (-> e { e.merge({ :foo => (-> e { 6 }).call(e) }) }).call(e) end }"
=end
If.new(Boolean.new(true),Assign.new(:foo,Number.new(3)),Assign.new(:foo,Number.new(6))).to_ruby
# => {:foo=>3}
proc = eval(
If.new(
Boolean.new(true),
Assign.new(:foo,Number.new(3)),
Assign.new(:foo,Number.new(6))
).to_ruby
)
proc.call({})
class CodeBlock < Struct.new(:first_statement, :second_statement)
def to_ruby
"-> e { (#{second_statement.to_ruby}).call((#{first_statement.to_ruby}).call(e)) }"
end
end
class While < Struct.new(:condition, :body)
def to_ruby
"-> e {" +
"while (#{condition.to_ruby}).call(e);" +
"e = (#{body.to_ruby}).call(e);end;" +
"e" +
"}"
end
end
=begin
=> "-> e {while (-> e { (-> e { e[:x] }).call(e) < (-> e { 3 }).call(e) }).call(e);
e = (-> e { e.merge({ :x => (-> e { (-> e { e[:x] }).call(e) + (-> e { 1 }).call(e) }).call(e) }) }).call(e);
end;e}"
=end
Assign.new(:x,Number.new(0))
statement = While.new(
LessThan.new(Variable.new(:x),Number.new(3)),
Assign.new(:x, Add.new(Variable.new(:x),Number.new(1)))
)
statement.to_ruby
# => {:x=>3}
proc = eval(statement.to_ruby)
proc.call({x: 1})
title: 程序的含义 date: 2017-10-15 10:30:46 tags:
程序语言理论
前言
编程语言，以及我们用编程语言所写的程序，这些都是软件工程师工作的基础。我们用编程语言和程序阐明复杂的想法，并在彼此间交流这些想法，当然最重要的是在计算机中实现这些想法。
程序员是注重实践实际的职业，他们通过阅读文档，学习教程，研究现有的程序以及修改自己的简单程序来学习新的编程语言，而不会过多的思考那些程序有什么含义。然而，计算机编程不单是与程序相关，重要的是程序员要表达思想。程序只是思想的静态表示，是曾经存在于程序员脑海中的某个结构的快照。程序是有了含义才值得写下来的。那么是什么把代码和它的含义连接在一起的呢？怎样才能能将一个程序的含义描述得更具体一点呢？
“含义”的含义
在语言学中，语义学(semantics)研究的是单词和它们含义之间的关系。比如，dog只是纸上一些符号的组合，或者由某人的声带引起的一系列空气震动，这与真正的狗或者通常意义上的狗的概念极为不同。语义不止关注抽象含义本身的基本性质，还关注具体的记号如何与它们抽象含义关联起来。
在计算机科学里，形式语义学偏向的是找到确定程序难以捉摸的含义的方法，并利用这些方法发现或者证明编程语言中有趣的东西。从定义新的编程语言和编译优化这种具体应用，到构造程序正确性的数学证明这样更抽象的领域，林林种种。这是一般的软件工程师接触不到的概念。
为了完整的定义编程语言，第一需要语法，描述程序看起来是什么样子；第二，语义，描述程序的含义。
但是许多语言都没有官方的书面规范，而只有一个可用的解释器或编译器。比如Ruby语言，它就没有标准规范，而是靠Matz先生的Ruby解释器(MRI)来规范的，也就是靠实现规范,任何一份Ruby的文档如果与MRI实际行为不一致，那么一定是文档错了。类似的语言还说有PHP和Perl。
另一些语言，是像C++，ECMAScript，Java描述编程语言的方法就是写一份平实的官方文档（一般是英文）。这些语言的标准化通过专家组成的委员会写成，与语言的实现无关，以至于这些语言的编译器解释器实现方式多种多样。通过官方规范定义一种语言更为严谨，这样所做的设计决策更有可能是经过深思熟虑的，而不是某一个特定实现的意外结果。但是语言标准规范，为了严谨化，通常非常难懂，文档中有没有矛盾，歧义的地方很难考证，这样的一份英文文档没有形式化的方法可以验证推导。
还有一种第三种方法来定义描述编程语言，就是使用形式语义学中的数学方法准确的描述编程语言的含义。这样的做法不仅能用适合系统分析甚至自动化分析的格式写出规范，还能保证其完全没有歧义，这样就可以对规范是否一致，是否含有冲突，以及是否有疏漏进行全面检查。
语法
传统的计算机程序是长长的字符串。每一种编程语言都有一系列的规则，描述那种语言中什么样的字符串被认为是有效程序。这些规则定义了这种语言的语法。
一个语法正确的程序能够被编译器正确的通过编译，也就是语法解析器能正确的处理这些字符串到一个抽象语法树(AST)，那么这些字符串就是语法正确的。
然而，语法关心的是程序的表面是什么样子，而不是它的含义。程序有可能语法正确但是没有任何实际意义。比如 z = "hello" + 1可能会在运行时甚至是编译器报错，因为它试图在一个字符串型的值上加数值型数据。这些含义就是解释器，编译器来决定的。取决于解释器怎么去解释它。
正如我们所料，能说明如何把一种编程语言的语法与这个语法所暗含的语义对应起来的唯一方法并不存在。实际上，关于程序的含义有几种不同的研究方法，它们都在形式化，抽象，可表达性和实际效率之间做了权衡。
操作语义
考虑程序含义的最实际方法是思考它做了什么：在运行程序的时候，我们期望发生什么，在编程语言运行时中的不同结构是如何表现的，把它们放到一起组成更大的程序时会是什么效果。
这是操作语义学的基础，这种方法为程序在某种机器上的执行定义一些规则，依次捕捉编程语言的含义。这个机器一般是一种抽象机器（可以简单理解为某种特殊的解释器）。
有了操作语义，就可以朝着严谨而准确地研究语言中特定结构的目标前进了。用英语写成的语言规范可能暗藏着二义性，但一个形式化的操作性规范不会如此。
小步语义
那么，如何设计一台抽象机器并使用它定义一种编程语言的操作语义呢？一种方法就是假想一台机器，用这台机器直接按照这种语言的语法进行操作一小步一小步地对其进行反复规约(Reduce)，从而对一个程序求值，无论最终结果如何，每一步都能让程序接近最终结果。
这种小步规约，类似数学中的代数求值:
(1 2) + (3 4) => 2 + (3 * 4) => 2 + 12 => 14
我们可以认为14就是最终结果，因为根据定义，14这样的具体值有自己的含义已经不能再进一步规约了。
把如何进行每一小步的规约写成形式化规则，这个非形式化的过程就可以转换成一个操作语义。这些规则本身需要用某种语言（元语言）写下来，一般来说，这样的语言是数学符号。
比如，以下就是某种语言（暂且成为Simple语言）采用小步语义的数学化描述:
（这里要加一个图片，小步语义的）
从逻辑上将，这是一个推导规则的集合，它定义了基于这个语言抽象语法树的一个规约关系。实际点讲，这是一堆怪异的符号，很难让人理解这些是什么东西。
现在我们不会试图直接理解讲解这种形式化的符号，而是研究如何利用程序设计语言编写同样的推导规则。当然据王垠所说,大部分的程序语言理论的论文里面都有这样大量的数学符号，让人眼花缭乱的逻辑公式，符号。如果你看透这些符号的本质，就会发现这些深奥的符号其实相当于解释器的代码，只不过是用一种晦涩难懂的形式化逻辑语言写出来的。所以呢，为了讲清楚这些符号背后的本质，我们直接通过可读性高的程序设计语言来直接构造推导关系。
如果有代码基础的人，这里可以看到我写的完整小步语义规约Simple语言的代码，是采用Ruby来构造的。
首先来研究下Simple语言中表达式的语义。规则将作用于这些表达式的抽象语法树，所以我们必须把Simple表达式表示成Ruby对象。要做到这一点，一种方式就是为了Simple语法中的每一种不同的元素定义一个Ruby类，包括数字，加法，乘法等。然后把每一个表达式表示成这些类的实例构造成一颗树。
下面是数字的加减乘除的Ruby代码:
为了测试以上代码的功能，手工实例化这些类来构造抽象语法树:
以上代码只会在控制台上打印表达式，但是不会对表达式进行计算，因为类中没有实现对应类的规约推导规则。
现在要为抽象语法树定义规约方法，这将是实现一个小步操作语义的起点。也就是说，代码可以以一个抽象语法树作为输入，然后生成一个规约树作为输出。
在实现规约之前，首先要区分什么是能规约的，什么是不能规约的。显然对于加减乘除这样的表达式总是能规约的，但是Number表达式总是代表一个具体数值，显然不能规约了。
下面就用类似组合子编程的思想来为每个表达式类编写规约的方法，每一个类判断自身是否能规约，并对自身类型作出规约的步骤，可以简单看成一种类型对应一个小型的解释器，它们只对自身的类型解释负责:
reduce方法总是构建出一个新的表达式，而不是对已有的进行修改。可以对其进行反复调用，从而通过很多步骤求出表达式的结果。
以上都是手工一步一步调用规约的，为了节省力气，可以用代码来模拟手工的规约操作，这是一个抽象机器，其实就是一个解释器，这个解释器自动对表达式进行规约求值。这是必然的，不然人类为啥要创造编译器，解释器这种东西呢？最简单的解释器无非就是一个函数或类，它接收一个表达式(输入)，然后规约到最终结果(输出)。
实例化一个虚拟机让它运行:
这个Simple语言的表达式解释到这里就完成了，但是这样的语言不是图灵完备的，因为程序还不支持控制流，就是有while，if，bool类型（与或非），大于小于等比较。要扩展很容易:
再次用虚拟机测试以上的代码:
以上代码按照意图正确规约到最终结果了。
是不是觉得完了？ 等等，一个正常的编程语言往往不会缺失变量这个语言特性吧？对，到现在，这门Simple语言还不支持变量！在任何有用的语言中，我们都期望在讨论值时能够使用有意义的名字，而不是它们本身的字面值(literal value)。所以我们引入一个新的表达式类Variable来支持变量:
变量是可以规约的，它只是值的名字，本质上变量与值是一个键值对的关系。所以它的规约很简单，就是在变量上下文中根据名字查找其对应的值，所以从最简单的构造，可以把这个环境上下文设计为一个Hash表的数据结构，Ruby有内建的表示了，所以很简单。
所以为了支持变量定义，加减乘除等表达式类的规约方法必须得接收一个变量上下文环境的参数:
虚拟机的类也必须跟着改动:
下面可以测试变量定义了:
有了变量，那么变量还必须支持赋值，其实赋值本质就是在不停的修改变量上下文环境而已。赋值是一条语句，一旦求值就改变了抽象机器的状态，机器的状态目前就是变量上下文环境了，也就是那个Hash表。最简单的语句就是什么也不做，它不能规约，因为不会改变任何状态:
一个什么都不做的语句看起来没有什么意义，但是有时表示程序已经执行成功完毕会非常方便。所以在其他语句完成了它们的工作之后，我会将它们最终规约成DoNothing。赋值语句的规约非常好写，无非就是接收一个表达式并规约表达式到一个不可规约状态，最后把最终的规约的值拿来修改一个变量的值:
手工对一个赋值表达式反复进行规约，直到终态:
通过抽象机器规约执行赋值语句:
到了现在，Simple语句还不完善，之前提到过，语言不支持控制流，因为有了bool型，那么现在就好实现if while循环这些特性了，另外还支持了代码块，一个代码块是由多条语句组成的:
以上代码使用小步语义的解决方式，使用代码块语句把while的一个级别展开，把它规约成一个只执行一次循环的if语句，然后再重复原始的while。
注意语句代码块支持两个语句，代码块可以嵌套，所以代码块支持多条语句组成的块。
如果程序支持语法有效但实际是错误的，那么按照之前写的代码，会崩溃,因为之前都没有考虑过一种情况:
以上代码是错误的，true 和 数值1不能相加。处理这个问题的一个方法就是在表达式能被规约的时候加入更多的约束，加入对求值失败可能性的考虑，这时求值过程可能终止，而不是总要试图规约成一个值，不然就可能崩溃，或者抛异常。
但是从实现者的角度考虑，我们可能不知道到参数的输入会是什么样子，加入这样的约束似乎很困难，从语法分析的角度是看不到这样的错误的，所以，最终，我们需要一个比语法更强大的工具，它能看到“未来”并让使用者，程序运行时避免执行任何可能崩溃或者终止处理的程序，这个就是大家可能听说过的静态分析。静态分析将采用一种静态语义(static semantics)的手段来根据语言的动态语义(dynamic semantics)来判断一个语法正确的程序是否具有有意义的含义。当然，这个就是语义分析。这篇文章到目前为止现在所讲解的都是程序的动态语义（操作语义）的内容，也就是说动态语义关注的是程序执行时具体做什么，到不关注程序这样做到底有没有意义。（这篇文章现在不会讲解静态分析的内容）
到目前未知，Simple语言支持了变量定义，赋值，if，while等基本的语言特性，与其他工业界的主流语言远远不能相比，它还不支持函数定义，函数调用等等功能。因为其环境上下文仅仅只是变量的Hash表键值对，不具有更强大的表达式关联。
小步语义的细节化，面向执行过程的风格能让它无歧义地定义真实世界上的所有编程语言。例如，Scheme语言的R6RS标准就使用了小步语义描述其执行，比提供了PLT Redex语言对这些语义进行参考实现。PLT Redex是一种用了设计和调试操作语义的一门DSL。 Ocaml语言在一个更简单的Core ML语言上构建了一系列的分层，也有对基础语言运行时行为的小步语义定义。
大步语义
我们已经看到小步语义是什么样子了。就是设计一台抽象机器维护一些执行状态，然后定义一些规约规则，这些规则详细说明了如何才能对每种程序结构循序渐进的求值。这样的做法，大部分都有迭代的味道，它要求抽象机器反复执行规约步骤，这些步骤以及与它们同样类型的信息可以作为自身的输入和输出，这让它们适合这种反复进行的应用程序。
这种小步的方法有一个优势，就是能把执行程序的复杂过程分成更小的片段进行解释和分析，但它却是有点不够直接：我们没有解释整个程序结构是如何工作的，而只是展示了它是如何慢慢规约的。为什么不能更直接地解释一个语句，完整地说明它的执行过程呢？这正是大步语义（big-step semantic）的依据。相对于小步语义的局部解释和分析颇有些全局解释分析的味道。
大步语义的思想是，定义如何从一个表达式或者语句直接得到它的结果。这必然需要把程序的执行当成一个递归而不是迭代的过程：大步语义说的是，为了对一个更大的表达式求值，我们要对所有比它小的子表达式求值，然后把结果结合起来得到最终答案。
在很多方面，这都比小步的方法更加自然，但确实失去了一些对细节的关注。例如，小步语义明确定义了操作应该发生的顺序，因为在每一步都明确了下一步规约应该是什么。但是大步语义经常会写成更为松散的形式，只会说哪些子计算会执行，而不会指明它们按照什么顺序执行。所以数学化地定义大步语义时，就不可避免地要讲清楚准确的求值策略了。
小步语义还提供给了一种轻松的方式用以监视计算的中间阶段的可能，而大步语义只返回一个结果，不会产生任何关于如何计算的证据。
为了理解这种权衡取舍，让我们回顾一些常见的语言结构，并看如何用Ruby来实现它的大步语义。我们之前的小步语义要求有一个AbstractMachine类来跟踪状态并反复执行规约，但是大步语义里，不需要这个类了。大步规约的规则描述了如何只对程序的抽象语法树访问一次就计算出整个程序的结果，因此不需要处理状态和重复。我们将只对表达式和语句类定义一个evaluate的求值方法，然后直接调用它。
表达式
处理小步语义时，我们不得不区分像1+2这样可以规约的表达式和像3这样不可规约的表达式，这样规约规则才能识别一个子表达式什么时候可以用来组成更大的程序。但是在大步语义中，每个表达式都能求值。唯一的区别，如果我们想要有个区别的话，就是对一些表达式求值会直接得到它们自身，而对另一些表达式求值会执行一些计算并得到一个不同的表达式。
大步语义的目标是像小步语义那样对一些运行时的行为建模，这意味着我们期望对于每一种程序结构，大步语义规则都要与小步语义规则程序最终生成的东西保持一致。从形式化上来说，就是把大小步语义这样的操作语义写成数学形式之后，这都是能被准确证明的。小步语义规则规定，像数值（Number）和布尔值（Boolean）这样的值不能在规约了，因此它们的大步规约非常简单：求值结果直接就是它们本身。
变量表达式是唯一的，这样它的小步语义允许它在成为一个值之前只规约一次，所以它的大步语义规则与小步规则一样，在变量环境中查找变量名，然后返回它的值。
二元表达式Add，Multiply和Lessthan等等，它们要求先对左右子表达式递归求值，然后再用恰当的运算合并两边结果值：
语句
在我们要定义语句的行为时，大步语义就能真正发挥作用了。在小步语义下表达式会规约成其他表达式，但语句会规约成do-nothing并且得到一个经过修改的变量环境。我们可以把大步语义的语句求值看成一个过程，这个过程总是把一个语句和一个初始化的变量环境转成一个最终环境，这避免了小步语义不得不对reduce产生的中间语句进行处理的复杂性。例如，对一个赋值语句的大步规约方法应该是完整地对其表达式进行求值，并返回一个包含结果值得更新了的变量环境：
类似地，DoNothing的evaluate方法无疑将把未修改的变量环境返回，而If类的evaluate方法的工作相当直接：对条件求值，然后把变量环境返回，这个变量环境来自于对序列或者代替语句求值得到的结果。
指称语义
到目前为止，我们已经从操作性方面观察了程序语言的含义，它通过展示程序执行之后发生的事情解释了程序的含义。而指称语义(denatational semantic)反而关心从程序的本来的语言到其他表示的转换。
这种类型的语义没有直接解释处理程序的执行，而是关注如何借助另一种语言（一般更低级，更形式化，至少比正在解释的语言更好理解）的已有含义来表示本来的语言。这样来看，这种语义可能近似于一种翻译器，但是，类似通常我们接触到的Less到CSS的转换，TypeScript到JavaScript的转换的理解。
指称语义是一种比操作语义更加抽象的方法，它不属于操作语义的范畴。它只是用一种语言替换成另一种语言，而不是像编译器或者解释器那样把一种语言转换成真实的行为。之前提到过，它更像一种翻译器，把中文转换为语义相同的英文，或者火星文。
指称语义通常用来把程序转化为更加形式化的数学对象语言，这样程序语言理论专家们就有了“共通的语言”来探讨问题了。
接下来我们需要把我们之前通过小步语义，大步语义定义的Simple语言转换到Ruby语言，实现Simple到Ruby的指称语义。
我们们可以用这个思想为Number类和Boolean类写一个to_ruby的实现，意思就是把这个结构翻译成对应的Ruby结构，这两种结构在语义上是等价的。Number和Boolean都是值的本身。
如果在Ruby console上运行以上代码:
这些to_ruby的方法每个都产生一个刚好包含Ruby程序代码的字符串表示，并且因为Ruby是一种我们理解其含义的语言，所以可以直接可以利用已有的Ruby解释器来eval这些Ruby程序字符串。
接下来，我们采用一致的思想写出变量，加减乘除等。变量麻，还是类似Hash表的上下文环境，通过变量名来查找变量对应的值：
加减乘除大于小于等操作符:
然后对以上代码进行测试:
Assign给变量赋值无非还是修改Hash表上下文环境:
DoNothing啥也不做，一个啥都不做的lambda表达式:
最后程序代码块，逻辑控制if while语句:
指称语义为一种语言实现了到另一种语言的翻译器，它提供了一个基础标准可以检验源语言的语义实现。
早期版本的Scheme标准使用指称语义来定义核心语言，而不是像现在的标准使用小步语义来定义。
总结---形式语义实践
小步语义，大步语义，指称语义它们三都可以用来定义程序语言，前两者属于操作语义，最后一者不属于。
关于形式化语义的研究，之前文章描述的都不正式，唯一正式的就是看到了那些稀奇古怪的逻辑符号，让大家不明觉厉。这样写作的方式是为了用更加浅显易懂，接地气的方式让大家了解什么是程序的含义。
形式化语义的一个重要应用就是为一种程序语言的含义给出一个无歧义的定义，本质上我们之前写的小步语义就相当于用Ruby语言重写了Simple语言的小步语义形式化定义，简单来说就是用通俗的Ruby语言重写实现了那些稀奇古怪的逻辑符号描述的无歧义的定义。
操作语义跟解释器很像，就像王垠大神所说，语义学虽然表面上是定义程序语言的含义，但其实就是研究各种各样的解释器（因为只有解释器解释才有了含义），那些稀奇古怪的逻辑符号本质上就是解释器代码，只不过那些代码用了很难理解的数学化符号编写定义了一种程序语言罢了。
所以，由于操作语义跟解释器很像，那么计算机科学家就可以把一个适当的解释器看成一种语言的操作语义，然后证明它在那种语言的指称语义方面的正确性------这意味着证明了由解释器给出的含义和由指称语义给出的含义之间存在着明显的联系。
指称语义的一个优点就是比操作语义抽象层次更高，它忽略了程序如何执行的细节，而只关心如何把它转换为一个不同的等价表示，这样带来的好处就是程序语言理论专家可以对不同语言写成的两个程序进行比较研究。
形式化的指称语义使用的是抽象的数学对象来表示表达式和语句这样的编程语言结构，并且因为数学上的约定会规定如何对函数求值这样的事情，这就有了一种直接在操作意义上思考指称的方式。我们已经用了野路子，把指称语义看作是一种语言到另一种语言的翻译器，而事实上这是大多数程序语言最终得以执行的方式，毕竟无论经过多少步骤转换，它们最终是要翻译成机器码，被送入到CPU解释成微指令，然后微指令又被放到一个CPU核心上执行的，然后再逐步向下到硅和电子的物理世界。这些程序语言信息经过这样一步一步转换会在什么地方结束呢？
语义这个抽象的高层建筑会逐步到达底部暴露出实际的机器：这些机器是什么样子的？ 可能是某种生物化学反应构造的计算装置，也可能是真正的量子计算机，也可能是现在目前造出的基于硅的半导体中的电子的物理机器，它们遵循的是物理法则。一台计算机是维护这个不确定结构的装置，大量复杂的解释层在彼此之上保持稳定。这就是计算理论有趣的地方------还是在说明抽象的重要性。
所以当我在谈论一种语言的语义或者某种语言特性时候，很少会提及它的实现，比如我现在已经很少提及C语言的局部变量是存放在栈空间的，malloc是在堆空间上分配的了，即使没有所谓的栈空间堆空间的概念了又怎样呢？难道我就不会C语言了吗？ 所以那种时候，反而我更加关注一种语言特性它能干什么？是带来了好处还是坏处？我会更加关注一个程序语言的官方规范标准(Specification)。
如果你深入研究你会发现文章提及过的语义类型都有其他别称。小步语义还叫结构化操作语义(structural operational semantic)和转换语义(transition semantic)。大步语义更普遍的叫法是自然语义(natural semantic)和关联语义(relational semantic)。而指称语义还可以称为不动点语义(fixed-point semantic)或者数学语义(mathematical semantic)。
还有其他类型的形式语义，其中一个是公理化语义(axiomatic semantic)，它通过在语句执行前后分别给出抽象机器状态的断言来描述一个语句的含义：如果一个断言（前置条件）在语句执行前初始化时true，那么随后的其他断言（后置条件）将是true。公理化语义在验证程序的正确性方面很有用：随着语句组合到一个更大的程序，它们对应的断言也可以组合成一个更大的断言，其目标就是表明对一个程序的总体断言与程序编写者的预期定义匹配。看到这里如果了解过程序语言理论的人脑袋可能会想起一种叫霍尔逻辑(Hoare logic)的概念。
公理化语义确实与这个相关。如果想了解，我就摘抄王垠大神写的《智能合约和形式验证》文章中的说法:
关于用这些形式验证系统，已经有很多实际应用了，因为有些领域确实需要安全性比较高的代码，一不小心除了问题就是大事，所以会非常注重程序代码的正确性，比如windows的驱动，高铁动车的调度系统，CPU的设计，还包括一些金融机构的核心交易系统都涉及到了形式验证来证明代码的正确。其中windows的驱动就有一种安全标注语言叫SAL，就是霍尔逻辑的一个实现。
实现语法分析器
学过编译原理这门课程的人都知道，实现一个编译器或者解释器都需要首先从词法分析，语法分析入手，到后面才是文章提到的语义分析相关的内容。为什么我可以直接开始讲语义部分呢？因为我们的Simple语言直接就是用类似抽象语法树的结构来编写的，类似于Lisp的代码结构:
这种类似树型的嵌套结构已经非常接近抽象语法树了，我们可以直接省略语法分析了，直接进入最重要的语义部分，这个部分涉及到程序变换，代码验证，代码优化，这是编译器的中端部分，这才是编译器和程序语言理论的精华。
编译器往往涉及了前端（词法分析，语法分析），中端（语义分析，类型系统，程序变换），后端（机器码生成，优化）。我认为现在中端对于我这篇文章才是最重要的，前端的实现涉及到状态机，各种文法理论，递归下降分析等各种分析方法固然是编程能力的体现，但是相对于中端就不是那么重要了，有现成的工具可用。后端也有现成的工具可用，比如LLVM,Rust语言和Swift语言的后端就是直接采用LLVM的。LLVM是当今最好的编译器后端框架。
编译器前端框架就多了，各种Parser Generator。比如，ANTLR,Bison, Lex & Yacc。 这些工具只要你写下自己设计的语言的BNF文法，就能帮助你生成对应的语法分析器了。如果你想自己手写词法分析和语法分析，那非常苦逼，恐怕你自己得补习下前端的相关理论了。这篇文章不会涉及。中端有没有相应的框架呢？ 没有，大部分中端的内容其实相当理论，要了解前沿恐怕需要去读论文。即使有相应的框架可能也只是涉及皮毛，解决不了多数问题，最重要也没有很著名的框架工具。知道为什么没有框架吗？因为前端后端已经是发展极为成熟的领域了，前端理论快被压榨干了，后端大部分都是机械化的处理数据，优化，生成。很难再出现什么新鲜的玩意了，虽然很复杂很难，但是估计也就那样了。中端到现在还有各种各样有趣的东西，各种语言特性，语义，类型系统都在这里被设计，是程序语言理论学家们研究的领域。各种论文层出不穷，各种方法理论，固然有换汤不换药的理论论文出来导致重复，但是还是一个正在发展的领域。
好了，这篇文章到此结束，我会写一个类似的系列。下一篇会讲自动机的理论，这涉及到词法分析的理论，也同样用Ruby演示。:)