taranovsky.rb

=begin
Usage: $ irb -r ./taranovsky.rb
irb(main):001:0> include Taranovsky
=> Object
irb(main):002:0> ZERO
=> 0 : ON
irb(main):003:0> ONE
=> C(0, 0) : ON
irb(main):004:0> ω
=> C(C(0, 0), 0) : ON
irb(main):005:0> Ω
=> Ω_1 : ON
irb(main):006:0> Omega.new(2)
=> Ω_2 : ON
irb(main):007:0> C.nat(3)
=> C(0, C(0, C(0, 0))) : ON
irb(main):008:0> ε_0 = C(Ω, 0)
=> C(Ω_1, 0) : ON
irb(main):009:0> ω < ε_0
=> true
irb(main):010:0> ε_0[C.nat 3]
=> C(C(C(0, 0), 0), 0) : ON
irb(main):011:0> he0 = Hardy(C(Ω, 0), 2)
=> H[C(Ω_1, 0)](2)
irb(main):012:0> he0 = he0.next
=> H[C(C(0, 0), 0)](2)
irb(main):013:0> he0 = he0.next
=> H[C(0, C(0, 0))](2)
irb(main):014:0> he0 = he0.next
=> H[C(0, 0)](3)
irb(main):015:0> he0 = he0.next
=> H[0](4)
irb(main):016:0> he0 = he0.value
=> 4
=end

module Taranovsky
  class Hardy
    attr_reader :a, :n

    def initialize(a, n)
      a = C.nat a if a.kind_of? Integer
      @a, @n = a, n
    end

    def inspect
      "H[#{a.to_s}](#{n.to_s})"
    end

    def value
      a, n = @a, @n
      loop do
        case a.cof
        when ZERO
          return n
        when ONE
          a = a[ZERO]
          n += 1
        else
          a = a[C.nat n]
        end
      end
    end

    def next
      case @a.cof
      when ZERO
        self
      when ONE
        Hardy.new(@a[ZERO], @n+1)
      else
        Hardy.new(@a[C.nat @n], @n)
      end
    end
  end

  def Hardy(a, n)
    Hardy.new(a, n)
  end

  class Ord
    def cof;end
    def base;end
    def [] n;end
    def to_a; [];end

    def < other
      x, y = to_a, other.to_a
      x.zip(y) do |(a, b)|
        return true if a < b
        return false if  a > b
      end
      return x.size < y.size
    end

    def === other; end

    def <= other
      self < other or self === other
    end

    def >= other
      not self < other
    end

    def > other
      self >= other and not self === other
    end

    def inspect
      "#{to_s} : ON"
    end
  end

  class Zero < Ord
    def cof
      self
    end
    def base
      self
    end
    def []
      raise "0 has no sequence"
    end
    def to_a
      [1]
    end

    def === other
      other.kind_of? Zero
    end

    def to_s
      '0'
    end
  end

  class Omega < Ord
    attr_reader :n
    def initialize(n = 1)
      @n = n
    end
    def cof
      self
    end
    def base
      self
    end
    def [](a)
      a
    end
    def to_a
      [@n+1]
    end
    def === other
      other.kind_of? Omega and other.n === @n
    end
    def to_s
      "Ω_#{@n}"
    end
  end

  class C < Ord
    attr_reader :a, :b

    def initialize(a, b)
      @a, @b = a, b
    end

    def self.nat(n)
      if n > 0
        C[ZERO, nat(n-1)]
      else
        ZERO
      end
    end

    def self.[](a, b)
      a = nat a if a.kind_of? Integer
      b = nat b if b.kind_of? Integer
      new(a, b)
    end

    def base
      @b.base
    end

    def cof
      case @a.cof
      when ZERO
        ONE
      when ONE
        OMEGA
      else
        if @a.base <= @b.base
          @a.cof
        else
          OMEGA
        end
      end
    end

    def [](n)
      case @a.cof
      when ZERO
        @b
      when ONE
        if n === ZERO
          @b
        else
          C[@a[0], self[n[0]]]
        end
      else
        if @a.base <= @b.base
          C[@a[n], @b]
        else
          if n === ZERO
            @b
          else
            C[@a[self[n[0]]], @b.base]
          end
        end
      end
    end

    def to_a
      @b.to_a + @a.to_a + [0]
    end

    def === other
      other.kind_of? C and @a === other.a and @b === other.b
    end

    def to_s
      "C(#{@a.to_s}, #{@b.to_s})"
    end
  end

  ZERO = Zero.new
  ONE = C[ZERO, ZERO]
  OMEGA_1 = Omega.new(1)
  OMEGA = C[ONE, ZERO]

  def C(a, b)
    C[a, b]
  end

  def Ω
    OMEGA_1
  end

  def ω
    OMEGA
  end
end