A Ruby interpreter for propositional logic

logical.rb

# frozen_string_literal: true

require "bundler/inline"

gemfile(true) do
  source "https://rubygems.org"

  git_source(:github) { |repo| "https://github.com/#{repo}.git" }

  gem "minitest"
end

require "minitest/autorun"

# simple propositional logic

class Token
  attr_reader :type, :value

  def initialize(type, value)
    @type = type
    @value = value
  end
end

class Lexer
  def initialize(input)
    @input = input
  end

  def tokens
    @input.split('').map do |char|
      # for each `char`, there are only 6 possible things to do
      case char
      when ' '
        next
      when '~'
        Token.new(:NOT, '~')
      when '&'
        Token.new(:AND, '&')
      when 'v'
        Token.new(:OR, 'v')
      when '>'
        Token.new(:IFSO, '>')
      when '('
        Token.new(:LPAREN, '(')
      when ')'
        Token.new(:RPAREN, ')')
      when 'T'
        Token.new(:TRUE, 'T')
      when 'F'
        Token.new(:FALSE, 'F')
      when *(('a'..'z').to_a - ['t', 'f', 'v'])
        Token.new(:VAR, char)
      end
    end.compact
  end
end

module AST
  class Atom
    attr_reader :value

    def initialize(value)
      @value = value
    end
  end
  
  class Variable
    attr_reader :value
  
    def initialize(value)
      @value = value
    end
  end

  class UnaryOperation
    attr_reader :operand

    def initialize(operand)
      @operand = operand
    end
  end

  class BinaryOperation
    attr_reader :left, :right

    def initialize(left, right)
      @left = left
      @right = right
    end
  end

  class Negation < UnaryOperation
  end

  class Conjunction < BinaryOperation
  end

  class Disjunction < BinaryOperation
  end

  class Implication < BinaryOperation
  end
end

class Parser
  def initialize(tokens)
    @tokens = tokens
    @stream = @tokens.to_enum
    @current_token = @stream.next
  end

  def parse
    expression
  end

  # expression :: disjunction (IFSO expression)*
  def expression
    result = disjunction
    token = @current_token

    if token.type == :IFSO
      eat(:IFSO)
      result = AST::Implication.new(result, expression)
    end

    result
  end

  # disjunction :: conjunction (OR disjunction)* 
  def disjunction
    result = conjunction
    token = @current_token

    if token.type == :OR
      eat(:OR)
      result = AST::Disjunction.new(result, disjunction)
    end

    result
  end

  # conjunction :: formula (AND conjunction)* 
  def conjunction
    result = formula
    token = @current_token

    if token.type == :AND
      eat(:AND)
      result = AST::Conjunction.new(result, conjunction)
    end

    result
  end

  # formula :: (NOT)* formula | LPAREN expression RPAREN | term
  def formula
    token = @current_token

    if token.type == :NOT
      eat(:NOT)
      return AST::Negation.new(formula)
    elsif token.type == :LPAREN
      eat(:LPAREN)
      result = expression
      eat(:RPAREN)
      return result
    else
      return term
    end
  end

  # term :: TRUE | FALSE | VAR
  def term
    token = @current_token

    if token.type == :TRUE
      eat(:TRUE)
      return AST::Atom.new(true)
    elsif token.type == :FALSE
      eat(:FALSE)
      return AST::Atom.new(false)
    elsif token.type == :VAR
      eat(:VAR)
      return AST::Variable.new(token.value)
    else
      raise "#{token.value} is an invalid term"
    end
  end

  def eat(token_type)
    raise 'ERROR' unless @current_token.type == token_type

    begin
      @current_token = @stream.next
    rescue StopIteration
    end
  end
end

class Interpreter
  def initialize(ast, context = {})
    @ast = ast
    @context = context
  end

  def interpret
    visit(@ast)
  end

  def visit(node)
    if node.is_a? AST::Atom
      visit_atom(node)
    elsif node.is_a? AST::Variable
      visit_variable(node)
    elsif node.is_a? AST::Negation
      visit_negation(node)
    elsif node.is_a? AST::Conjunction
      visit_conjunction(node)
    elsif node.is_a? AST::Disjunction
      visit_disjunction(node)
    elsif node.is_a? AST::Implication
      visit_implication(node)
    end
  end

  def visit_atom(node)
    node.value
  end
  
  def visit_variable(node)
    @context[node.value]
  end

  def visit_negation(node)
    case visit(node.operand)
    when true
      false
    when false
      true
    end
  end

  def visit_conjunction(node)
    case [visit(node.left), visit(node.right)]
    when [false, false]
      false
    when [false, true]
      false
    when [true, false]
      false
    when [true, true]
      true
    end
  end

  def visit_disjunction(node)
    case [visit(node.left), visit(node.right)]
    when [false, false]
      false
    when [false, true]
      true
    when [true, false]
      true
    when [true, true]
      true
    end
  end

  def visit_implication(node)
    case [visit(node.left), visit(node.right)]
    when [false, false]
      true
    when [false, true]
      true
    when [true, false]
      false
    when [true, true]
      true
    end
  end
end

class Expression
  def initialize(string)
    @string = string
  end
  
  def resolve
    interpreter = Interpreter.new(ast)
    interpreter.interpret
  end
  
  def given(context)
    interpreter = Interpreter.new(ast, context)
    interpreter.interpret
  end
  
  def truth_table
    table = {}
    [true, false].repeated_permutation(variables.count).each do |booleans|
      context = Hash[variables.zip(booleans)]
      table[context] = given(context)
    end
    table
  end
  
  def variables = tokens.select { |t| t.type == :VAR }.map(&:value)
  def tokens = Lexer.new(@string).tokens
  def ast = Parser.new(tokens).parse
end

# -----------------------------------------------------------------------------

class LogicInterpreterTest < Minitest::Test
  def test_tokens
    assert_equal true, Expression.new('T').resolve
    assert_equal false, Expression.new('F').resolve
  end
  
  def test_negation
    assert_equal false, Expression.new('~T').resolve
    assert_equal true, Expression.new('~F').resolve
  end
  
  def test_conjunction
    assert_equal true, Expression.new('T & T').resolve
    assert_equal false, Expression.new('T & F').resolve
    assert_equal false, Expression.new('F & T').resolve
    assert_equal false, Expression.new('F & F').resolve
  end
  
  def test_disjunction
    assert_equal true, Expression.new('T v T').resolve
    assert_equal true, Expression.new('T v F').resolve
    assert_equal true, Expression.new('F v T').resolve
    assert_equal false, Expression.new('F v F').resolve
  end
  
  def test_implication
    assert_equal true, Expression.new('T > T').resolve
    assert_equal false, Expression.new('T > F').resolve
    assert_equal true, Expression.new('F > T').resolve
    assert_equal true, Expression.new('F > F').resolve
  end
  
  def test_simple_expressions
    assert_equal false, Expression.new('~F & F').resolve
    assert_equal false, Expression.new('F v ~T').resolve
  end
  
  def test_stacked_negations
    assert_equal true, Expression.new('~~T').resolve
    assert_equal true, Expression.new('~~~F').resolve
    assert_equal false, Expression.new('~~F & F').resolve
    assert_equal true, Expression.new('F v ~~T').resolve
  end
  
  def test_parenthetical_grouping
    assert_equal true, Expression.new('T & (F v T)').resolve
    assert_equal false, Expression.new('~(T & (F v T))').resolve
    assert_equal true, Expression.new('~(T & (F v T)) > T').resolve
  end
  
  def test_operator_precedence
    assert_equal true, Expression.new('T & F v T').resolve
    assert_equal false, Expression.new('T & F v ~T').resolve
    assert_equal true, Expression.new('F & T v T').resolve
    assert_equal true, Expression.new('~F & T v T').resolve
  end
end

class LogicExpressionTest < Minitest::Test
  def test_variable
    assert_equal(
      {{"p"=>true}=>true, {"p"=>false}=>false},
      Expression.new('p').truth_table
    )
  end
  
  def test_negation
    assert_equal(
      {{"p"=>true}=>false, {"p"=>false}=>true},
      Expression.new('~p').truth_table
    )
  end
  
  def test_conjunction
    assert_equal(
      {{"p"=>true, "q"=>true}=>true,
       {"p"=>true, "q"=>false}=>false,
       {"p"=>false, "q"=>true}=>false,
       {"p"=>false, "q"=>false}=>false},
      Expression.new('p & q').truth_table
    )
  end
  
  def test_disjunction
    assert_equal(
      {{"p"=>true, "q"=>true}=>true,
       {"p"=>true, "q"=>false}=>true,
       {"p"=>false, "q"=>true}=>true,
       {"p"=>false, "q"=>false}=>false},
      Expression.new('p v q').truth_table
    )
  end
  
  def test_implication
    assert_equal(
      {{"p"=>true, "q"=>true}=>true,
       {"p"=>true, "q"=>false}=>false,
       {"p"=>false, "q"=>true}=>true,
       {"p"=>false, "q"=>false}=>true},
      Expression.new('p > q').truth_table
    )
  end
  
  def test_simple_expressions
    assert_equal(
      {{"p"=>true, "q"=>true}=>false,
       {"p"=>true, "q"=>false}=>false,
       {"p"=>false, "q"=>true}=>true,
       {"p"=>false, "q"=>false}=>false},
      Expression.new('~p & q').truth_table
    )
  end
  
  def test_stacked_negations
    assert_equal(
      {{"p"=>true}=>true, {"p"=>false}=>false},
      Expression.new('~~p').truth_table
    )
    assert_equal(
      {{"p"=>true, "q"=>true}=>true,
       {"p"=>true, "q"=>false}=>false,
       {"p"=>false, "q"=>true}=>false,
       {"p"=>false, "q"=>false}=>false},
      Expression.new('~~p & q').truth_table
    )
    assert_equal(
      {{"p"=>true, "q"=>true}=>true,
       {"p"=>true, "q"=>false}=>true,
       {"p"=>false, "q"=>true}=>true,
       {"p"=>false, "q"=>false}=>false},
      Expression.new('~~p v q').truth_table
    )
    assert_equal(
      {{"p"=>true, "q"=>true}=>true,
       {"p"=>true, "q"=>false}=>false,
       {"p"=>false, "q"=>true}=>true,
       {"p"=>false, "q"=>false}=>true},
      Expression.new('~~p > q').truth_table
    )
  end
  
  def test_parenthetical_grouping
    assert_equal(
      {{"p"=>true, "q"=>true, "r"=>true}=>true,
       {"p"=>true, "q"=>true, "r"=>false}=>true,
       {"p"=>true, "q"=>false, "r"=>true}=>true,
       {"p"=>true, "q"=>false, "r"=>false}=>false,
       {"p"=>false, "q"=>true, "r"=>true}=>false,
       {"p"=>false, "q"=>true, "r"=>false}=>false,
       {"p"=>false, "q"=>false, "r"=>true}=>false,
       {"p"=>false, "q"=>false, "r"=>false}=>false},
      Expression.new('p & (q v r)').truth_table
    )
    assert_equal(
      {{"p"=>true, "q"=>true, "r"=>true}=>false,
       {"p"=>true, "q"=>true, "r"=>false}=>false,
       {"p"=>true, "q"=>false, "r"=>true}=>false,
       {"p"=>true, "q"=>false, "r"=>false}=>true,
       {"p"=>false, "q"=>true, "r"=>true}=>true,
       {"p"=>false, "q"=>true, "r"=>false}=>true,
       {"p"=>false, "q"=>false, "r"=>true}=>true,
       {"p"=>false, "q"=>false, "r"=>false}=>true},
      Expression.new('~(p & (q v r))').truth_table
    )
    assert_equal(
      {{"p"=>true, "q"=>true, "r"=>true, "s"=>true}=>true,
       {"p"=>true, "q"=>true, "r"=>true, "s"=>false}=>true,
       {"p"=>true, "q"=>true, "r"=>false, "s"=>true}=>true,
       {"p"=>true, "q"=>true, "r"=>false, "s"=>false}=>true,
       {"p"=>true, "q"=>false, "r"=>true, "s"=>true}=>true,
       {"p"=>true, "q"=>false, "r"=>true, "s"=>false}=>true,
       {"p"=>true, "q"=>false, "r"=>false, "s"=>true}=>true,
       {"p"=>true, "q"=>false, "r"=>false, "s"=>false}=>false,
       {"p"=>false, "q"=>true, "r"=>true, "s"=>true}=>true,
       {"p"=>false, "q"=>true, "r"=>true, "s"=>false}=>false,
       {"p"=>false, "q"=>true, "r"=>false, "s"=>true}=>true,
       {"p"=>false, "q"=>true, "r"=>false, "s"=>false}=>false,
       {"p"=>false, "q"=>false, "r"=>true, "s"=>true}=>true,
       {"p"=>false, "q"=>false, "r"=>true, "s"=>false}=>false,
       {"p"=>false, "q"=>false, "r"=>false, "s"=>true}=>true,
       {"p"=>false, "q"=>false, "r"=>false, "s"=>false}=>false},
      Expression.new('~(p & (q v r)) > s').truth_table
    )
  end
  
  def test_operator_precedence
    assert_equal(
      {{"p"=>true, "q"=>true, "r"=>true}=>true,
       {"p"=>true, "q"=>true, "r"=>false}=>true,
       {"p"=>true, "q"=>false, "r"=>true}=>true,
       {"p"=>true, "q"=>false, "r"=>false}=>false,
       {"p"=>false, "q"=>true, "r"=>true}=>true,
       {"p"=>false, "q"=>true, "r"=>false}=>false,
       {"p"=>false, "q"=>false, "r"=>true}=>true,
       {"p"=>false, "q"=>false, "r"=>false}=>false},
      Expression.new('p & q v r').truth_table
    )
    assert_equal(
      {{"p"=>true, "q"=>true, "r"=>true}=>true,
       {"p"=>true, "q"=>true, "r"=>false}=>true,
       {"p"=>true, "q"=>false, "r"=>true}=>false,
       {"p"=>true, "q"=>false, "r"=>false}=>true,
       {"p"=>false, "q"=>true, "r"=>true}=>false,
       {"p"=>false, "q"=>true, "r"=>false}=>true,
       {"p"=>false, "q"=>false, "r"=>true}=>false,
       {"p"=>false, "q"=>false, "r"=>false}=>true},
      Expression.new('p & q v ~r').truth_table
    )
    assert_equal(
      {{"p"=>true, "q"=>true, "r"=>true}=>true,
       {"p"=>true, "q"=>true, "r"=>false}=>false,
       {"p"=>true, "q"=>false, "r"=>true}=>true,
       {"p"=>true, "q"=>false, "r"=>false}=>false,
       {"p"=>false, "q"=>true, "r"=>true}=>true,
       {"p"=>false, "q"=>true, "r"=>false}=>true,
       {"p"=>false, "q"=>false, "r"=>true}=>true,
       {"p"=>false, "q"=>false, "r"=>false}=>false},
      Expression.new('~p & q v r').truth_table
    )
  end
end