Re: What is OOP?

On Mon, 2024-12-09 at 08:28 +0800, wij wrote:

On Sun, 2024-12-08 at 17:56 +0000, Isaac Ganoung wrote:

On Mon, 02 Dec 2024 08:57:41 +0800, wij wrote:
 

How do you verify correctness just by the program 'logic'?

 
You use a functional language like Haskell. You are probably looking for
this: https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence

 
I don't know what to look for, maybe this is from another olcott, knowing
nothing of what he quotes.
So far, I feel C++ is the best language to model general problems.
 
The following is in response to the example in the provided webpage (if the
problem is simple or from a selected set, there are generally various kind
of elegant solutions):
 
------------------------------------
#include <Wy.stdio.h>
#include <Sc/Search.h>
 
using namespace Wy;
using namespace Sc;
#include "Sc/TestRule.inc" // This file must be included after the above using...
 
const SubstiRule rule_fac0(fac(NatNum_0), NatNum_1); // fac(0) -> 1
const SubstiRule rule_fac1(fac(UVarN_n), UVarN_n*fac(UVarN_n-NatNum_1)); // fac(n) -> n*fac(n-1)
 
RuleSet rule;
 
// Make rule from "Sc/TestRule.inc" and add two rules
void make_rule() {
 Errno r;
 for(size_t ri=0; ri<sizeof(brule)/sizeof(brule[0]); ++ri) {
   if((r=rule.add_rule(brule[ri]))!=Ok) {
     WY_THROW(r);
   }
 }
 if((r=rule.add_rule(rule_fac0))!=Ok) {
   WY_THROW(r);
 }
 if((r=rule.add_rule(rule_fac1))!=Ok) {
   WY_THROW(r);
 }
 
 // dump the final rule
 cout << "-------- Rules ---------" << WY_ENDL;
 for(size_t i=0; i<rule.num_rules(); ++i) {
   cout << '(' << wrd(i) << ") "
        << wrd(rule.rule(i).match_pattern()) << " -> "
        << wrd(rule.rule(i).deduct_pattern()) << WY_ENDL;
 }
 cout << "-----------------" << WY_ENDL;
};
 
void t0() {
 Errno r;
 make_rule();
 Search sr0(rule);
 const DyExpr ini_expr=fac(NatNum_2);
 const DyExpr des_expr=NatNum_2;
 
 cout << "Compute: " << wrd(ini_expr) << " -> " << wrd(des_expr) << WY_ENDL;
 if((r=sr0.search(ini_expr,des_expr,10,Search::Mode::Shortest))!=Ok) {
   WY_THROW(r);
 }
 const Array<Step>& garr= sr0.gpath();
 if(garr.is_empty()) {
   cout << "goal is not found" WY_ENDL;
 } else {
   cout << garr.size() << " steps" WY_ENDL;
   for(size_t i=0; i<garr.size(); ++i) {
     cout << '(' << garr[i].rule_index() << ") " << wrd(garr[i].expr()) << WY_ENDL;
   }
 }
};
 
int main()
try {
 cout << "check " __FILE__ WY_ENDL;
 t0();
 cout << "OK" WY_ENDL;
 return 0;
}
catch(const Errno& e) {
 cerr << wrd(e) << WY_ENDL;
 return -1;
}
catch(...) {
 cerr << "main caught(...)" WY_ENDL;
 return -1;
};
-----------------------
[]$ g++ a_fac.cpp -lwy
[]$ ./a.out
 
check a_fac.cpp
-------- Rules ---------
(0) (_a+_b) -> (_b+_a)
(1) (_a+(_b+_c)) -> ((_a+_b)+_c)
(2) ((_a+_b)+_c) -> (_a+(_b+_c))
(3) (_a+0) -> _a
(4) (_a-_b) -> (_a+(-_b))
(5) (_a+(-_b)) -> (_a-_b)
(6) (_a-_a) -> 0
(7) (-(_a+_b)) -> ((-_a)+(-_b))
(8) ((-_a)+(-_b)) -> (-(_a+_b))
(9) (-(-_a)) -> _a
(10) (-0) -> 0
(11) (_a*_b) -> (_b*_a)
(12) (_a*(_b*_c)) -> ((_a*_b)*_c)
(13) ((_a*_b)*_c) -> (_a*(_b*_c))
(14) (_a*(_b+_c)) -> ((_a*_b)+(_a*_c))
(15) ((_a*_b)+(_a*_c)) -> (_a*(_b+_c))
(16) (_a*1) -> _a
(17) (_a*0) -> 0
(18) (_a/_b) -> (_a*(1/_b))
(19) (_a*(1/_b)) -> (_a/_b)
(20) (_a/_a) -> 1
(21) (_a/0) -> $Und_D0
(22) (-(_a*_b)) -> ((-_a)*_b)
(23) ((-_a)*_b) -> (-(_a*_b))
(24) (_a*(-_b)) -> ((-_a)*_b)
(25) ((-_a)*_b) -> (_a*(-_b))
(26) ((-_a)*(-_b)) -> (_a*_b)
(27) (-(_a/_b)) -> ((-_a)/_b)
(28) ((-_a)/_b) -> (-(_a/_b))
(29) (_a/(-_b)) -> ((-_a)/_b)
(30) ((-_a)/_b) -> (_a/(-_b))
(31) ((-_a)/(-_b)) -> (_a/_b)
(32) (_a^0) -> 1
(33) (_a^1) -> _a
(34) (_a^_b) -> (_a*(_a^(_b-1)))
(35) ((_a*_b)^_c) -> ((_a^_c)*(_b^_c))
(36) (_a^(_b+_c)) -> ((_a^_b)*(_a^_c))
(37) (_a^(_b*_c)) -> ((_a^_b)^_c)
(38) (0^_a) -> $Und_B0
(39) (_a^(-_b)) -> (1/(_a^_b))
(40) (2-1) -> 1
(41) (_a*_a) -> (_a^2)
(42) (_a+_a) -> (2*_a)
(43) fac(0) -> 1
(44) fac(_n) -> (_n*fac((_n-1)))
-----------------
Compute: fac(2) -> 2
7 steps
(44) (2*fac((2-1)))
(40) (2*fac(1))
(44) (2*(1*fac((1-1))))
(6) (2*(1*fac(0)))
(43) (2*(1*1))
(16) (2*1)
(16) 2
OK
 
----------------
Common criticism of libwy is the many error check codes.
But I feel such codes are necessary in real programs, hiding
it is dishonest.

Have you found that rule [40] is strange? From there, already, stories can be
told about math. and logic (and C++, but more abstract).

Note: I did not comment Haskell, sine I know nealy nothing of it and wish to
      understand what is really there.