exercise_5

#!/usr/bin/env ruby

require 'bundler/setup'
require 'satre'
require 'terminal-table'

include Satre

problem_5_1_1_1 = 'g(d,d)'.to_term
problem_5_1_1_2 = 'f(x,g(y,z),d)'.to_term
problem_5_1_1_3 = 'g(x,f(y,z),d)'.to_term
problem_5_1_1_4 = 'f(x,h(x,z),d)'.to_term
sig_5_1_1 = {d: 0, f: 2, g: 3}

problem_5_1_2_1 = 'S(m, x)'.to_formula
problem_5_1_2_2 = 'B(m, f(m))'.to_formula
problem_5_1_2_3 = 'B(B(m,x),y)'.to_formula
problem_5_1_2_4 = 'B(x,y) ==> (exists z. S(z,y))'.to_formula
problem_5_1_2_5 = 'S(x,y) ==> S(y,f(f(x)))'.to_formula
sig_5_1_2 = {m: 0, f: 1, S: 2, B: 2}

axiom_1 = "forall x. x = x".to_formula
axiom_2 = "forall x y. (x = y ==> y = x)".to_formula
axiom_3 = "forall x y z. (x = y /\\ y = x ==> x = z)".to_formula

domain = (0..23).to_a
valudation = {}
func = ->(f, args) {}
empty = ->(p, args) { if p == '=' then false else fail "undefined predicate #{p}" end }
universal = ->(p, args) { if p == '=' then true else fail "undefined predicate #{p}" end }
equality = ->(p, args) { if p == '=' then args.inject(:==) else fail "undefined predicate #{p}" end }
even_sum = ->(p, args) { if p == '=' then args.inject(:+).even? else fail "undefined predicate #{p}" end }
modular_aritmetic = ->(p, args) { if p == '=' then args[0] == (args[1] % 16) else fail "undefined predicate #{p}" end }

problem_5_1_1 = Terminal::Table.new do |t|
  t.title = 'Problem 5.1.1'
  t.headings = ['', 'Term', 'Signature', 'wellformed?']
  t << ['1.', problem_5_1_1_1, sig_5_1_1.to_s, problem_5_1_1_1.wellformed?(sig_5_1_1) ]
  t << ['2.', problem_5_1_1_2, sig_5_1_1.to_s, problem_5_1_1_2.wellformed?(sig_5_1_1) ]
  t << ['3.', problem_5_1_1_3, sig_5_1_1.to_s, problem_5_1_1_3.wellformed?(sig_5_1_1) ]
  t << ['4.', problem_5_1_1_4, sig_5_1_1.to_s, problem_5_1_1_4.wellformed?(sig_5_1_1) ]
end

problem_5_1_2 = Terminal::Table.new do |t|
  t.title = 'Problem 5.1.2'
  t.headings = ['', 'Formula', 'Signature', 'wellformed?']
  t << ['1.', problem_5_1_2_1, sig_5_1_2.to_s, problem_5_1_2_1.wellformed?(sig_5_1_2) ]
  t << ['2.', problem_5_1_2_2, sig_5_1_2.to_s, problem_5_1_2_2.wellformed?(sig_5_1_2) ]
  t << ['3.', problem_5_1_2_3, sig_5_1_2.to_s, problem_5_1_2_3.wellformed?(sig_5_1_2) ]
  t << ['4.', problem_5_1_2_4, sig_5_1_2.to_s, problem_5_1_2_4.wellformed?(sig_5_1_2) ]
  t << ['5.', problem_5_1_2_5, sig_5_1_2.to_s, problem_5_1_2_5.wellformed?(sig_5_1_2) ]
end

problem_5_2 = Terminal::Table.new do |t|
  t.title = 'Problem 5.2'
  t.headings = ['relation', "#{axiom_1}.holds?", "#{axiom_2}.holds?", "#{axiom_3}.holds?"] 
  t << ['empty', axiom_1.holds?(domain, func, empty, valudation), axiom_2.holds?(domain, func, empty, valudation), axiom_3.holds?(domain, func, empty, valudation)]
  t << ['universal', axiom_1.holds?(domain, func, universal, valudation), axiom_2.holds?(domain, func, universal, valudation), axiom_3.holds?(domain, func, universal, valudation)]
  t << ['equality', axiom_1.holds?(domain, func, equality, valudation), axiom_2.holds?(domain, func, equality, valudation), axiom_3.holds?(domain, func, equality, valudation)]
  t << ['even sum', axiom_1.holds?(domain, func, even_sum, valudation), axiom_2.holds?(domain, func, even_sum, valudation), axiom_3.holds?(domain, func, even_sum, valudation)]
  t << ['modular aritmetic', axiom_1.holds?(domain, func, modular_aritmetic, valudation), axiom_2.holds?(domain, func, modular_aritmetic, valudation), axiom_3.holds?(domain, func, modular_aritmetic, valudation)]
end

puts """
Problem 5.1.1

Represent the signature definition F (and its arities) in Problem 5.1.1. Note
that a constant is defined as a function with no argument. Next, implement
a function

  wellformed_term :: Term ==> Signature ==> Bool

which has a term and a signature as its arguments, and checks whether it is
well-formed according to the signature or neot. The definition of whether a
term t is well-formed with respect to signature sig is defined as follows:

  (1.) A variable x is well-formed.
  (2.) A term f(x_1,...,x_n) is well-formed if
    (a.) Each term x_1,...,x_n is well-formed
    (b.) There is a pair (s, m) in signature sig where s = t and n = m

By using the definition of wellformedness above, check whether each expression
in the Problem 5.1.1. is well-formed or not. Note that you need to use 
parset (String#to_term) instead of parse (String#to_formula) function.
Check your answer with the pencil-and-paper solutions.

Answer:

#{problem_5_1_1}

Represent first the signature in Problem 5.1.2. Then, define a function

  wellformed_form :: Formula Fol ==> Signature ==> Bool

Which has a first-order formula and a signature as its argument,
and checks whether it is well-formed according to the signature or not.
The definition whether a formula is well-formed with respect to the signature
sig is defined as follows:

  (1.) Constant True and False are well-formed
  (2.) Predicate p(x_1,...,x_n) is well-formed if
    (a.) each term x_1,...,x_n is well-formed
    (b.) There is a pair (q,m) in signature sig where q = p and n = m
  (3.) p X q where X element {/\\,\\/,==>,<=>} is well-formed if p and q are 
       well-formed
  (4.) forall x.p and exsists x.p are well-formed if p is well-formed

By using the definition of wellformedness above, check wheter each expression in
the Problem 5.1.2. is well-formed or not. Check your answer with the prencil-
and-paper derivation.

Answer:

#{problem_5_1_2}

Problem 5.2

In this part, we shall check mechanically whether an interpretation satisfies
the equivalence relation's axiom or not. However, since the definiton can
be used in the domain is finite, we set the domain for this programming exercise
to be {0,1,...,23}

  (1.) Parse first Axiom 1, 2, and 3 in Problem 5.2.
  (2.) Implement the predicate for each possible mappings of predicate =.
       That is, implement the function for empty, universal, equality, even sum,
       and modular aritmetic relation.
  (3.) Check for each possible mapping of predicate =, whether Axiom 1, 2, or 3
       is true.

Answer:

#{problem_5_2}

(c) Roman Podolski, Technische Universität München, January 2016
"""