Diff with http://xaviershay.github.io/writing/docs/1_sos.html to collapse `apply?` and `reducible?` into an identity function. I'm currently thinking I will introduce this after I've had to introduce equality definitions for a different reason. For the purposes of explaining the mathematical notation, I feel like it is unnecessary conceptual ove…

gistfile1.diff

diff --git a/code/1_sos.rb b/code/1_sos.rb
index 03bd37e..8de6d9b 100644
--- a/code/1_sos.rb
+++ b/code/1_sos.rb
@@ -34,7 +34,8 @@ end
 Number = Struct.new(:value) do
   def to_s;       value.to_s end
   def inspect;    "«#{self}»" end
-  def reducible?; false end
+  def ==(other);  other.is_a?(Number) && value == other.value end
+  def reduce(env); [self, env] end
 end
 
 exp, env = Number[10], {} # => [«10», {}]
@@ -44,7 +45,9 @@ exp, env = Number[10], {} # => [«10», {}]
 Add = Struct.new(:left, :right) do
   def to_s;       "%s + %s" % [left, right] end
   def inspect;    "«#{self}»" end
-  def reducible?; true end
+  def ==(other)
+    other.is_a?(Add) && [left, right] == [other.left, other.right]
+  end
   def reduce(env)
     [Number.new(left.value + right.value), env, :addition]
   end
@@ -64,15 +67,19 @@ class Add
   end
 
   def reduce(env)
-    rule = self.class.rules.detect {|r| r.apply?(self) }
+    rule = self.class.rules.detect {|r| r.apply(self, env) != [self, env] }
+    raise "No rule applies" unless rule
     rule.apply(self, env) << rule
   end
 end
 
 AddValues = Struct.new(:expression_type) do
-  def apply?(*args); true end
   def apply(add, env)
-    [Number[add.left.value + add.right.value], env]
+    if add.left.is_a?(Number) && add.right.is_a?(Number)
+      [Number[add.left.value + add.right.value], env]
+    else
+      [add, env]
+    end
   end
 end
 
@@ -130,8 +137,11 @@ end
 
 def evaluate(exp, env = {})
   print_line exp, env, nil
-  while exp.reducible?
+  last = nil
+  while true
+    last = [exp, env]
     exp, env, rule = exp.reduce(env)
+    break if last == [exp, env]
     print_line exp, env, format_rule(rule)
   end
 rescue => e
@@ -144,7 +154,6 @@ evaluate Add[ Number[1], Number[2] ]
 #     «1 + 2», {} |
 #         «3», {} | <x + y, σ> → <z, σ> if z is the sum of x and y
 
-
 # Our operational semantics now contains only one rule: that of
 # addition. What happens in the following case?
 
@@ -169,7 +178,6 @@ class Add
 end
 
 ReduceArgument = Struct.new(:expression_type, :n) do
-  def apply?(exp); exp[n].reducible?  end
   def apply(exp, env)
     r =  exp.each.map.with_index {|x, i|
       i == n ? x.reduce(env)[0] : x