Sequent calculus: universal quantification

[Neal Alexander]

Is there a better way to prove the associativity of a function other than brute-force examining all elements of a 'representative' subset of it's domain?

Its fine for u2 below, since <(list A), append> is a free monoid and can ignore the values of the underlying set, but it is kind of unsatisifying in the general case.

\\ negation

(datatype ~

                                  A; !; fail!;

                             _____________________

                                     (~ A);

                             _____________________

                                    (~ A); )

\\ collect list of elements generated by F

(datatype collect

                                     (F X);

                                (collect F XS);

                           _________________________

                             (collect F (X | XS));

                           _________________________

                                (collect _ ());)

\\ universal quantification

(datatype forall

                                (collect U XS);

                                     (~ P);

                            _______________________

                               (forall-h XS U P);

                    \\ make sure U doesn't fail prematurely

                                     (U _);

                             (~ (forall-h XS U P));

                             _____________________

                               (forall XS U P); )

\\ algebraic laws

(datatype associative

                             let F (function Join)

                              if (= (F A (F B C))

                                    (F (F A B) C))

                     _____________________________________

                          (associative-h Join A B C);

                (forall (A B C) Set (associative-h Join A B C));

             _____________________________________________________

                           (associative Set Join); )

\\ an algebraic structure

(datatype semigroup

                            (associative Set Join);

                 _____________________________________________

                    [semigroup Set Join] : (semigroup Set);)

Test session

(5+) (tc +)

true

(6+) (datatype universe

                            _______________________

                                     (u 1);

                            _______________________

                                     (u 2);

                            _______________________

                                    (u 3);)

type#universe

(7+) [semigroup u *] : (semigroup u)

[semigroup u *] : (semigroup u)

(8+) [semigroup u +] : (semigroup u)

[semigroup u +] : (semigroup u)

(9+) [semigroup u -] : (semigroup u)

type error

(10+) [semigroup u /] : (semigroup u)

type error

(11+) (datatype universe-2

                            _______________________

                                    (u2 []);

                            _______________________

                                   (u2 [1]);

                            _______________________

                                  (u2 [2 3]);)

type#universe-2 : symbol

(12+) [semigroup u2 append] : (semigroup u2)

[semigroup u2 append] : (semigroup u2)

[Mark Tarver]

I think that proving the associativity of a function in the general case requires inductive proof and human assistance.  For finite domains you can take a different appraoch.

https://groups.google.com/forum/?hl=en#!searchin/qilang/semigroup%7Csort:date/qilang/D3tmhQvfnOE/fKgddlbhWxwJ  might help.

Mark

--
You received this message because you are subscribed to the Google Groups "Shen" group.
To unsubscribe from this group and stop receiving emails from it, send an email to qilang+unsubscribe@googlegroups.com.
To post to this group, send email to qil...@googlegroups.com.
Visit this group at https://groups.google.com/group/qilang.
For more options, visit https://groups.google.com/d/optout.