Groups | Search | Server Info | Keyboard shortcuts | Login | Register [http] [https] [nntp] [nntps]

Groups > comp.lang.c++ > #121168

Re: What is OOP?

Show all headers | View raw

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.

Back to comp.lang.c++ | Previous | Next — Previous in thread | Next in thread | Find similar | Unroll thread

Thread

What is OOP? wij <wyniijj5@gmail.com> - 2024-12-02 01:17 +0800
  Re: What is OOP? Ross Finlayson <ross.a.finlayson@gmail.com> - 2024-12-01 10:43 -0800
    Re: What is OOP? Ross Finlayson <ross.a.finlayson@gmail.com> - 2024-12-01 10:49 -0800
  Re: What is OOP? Lynn McGuire <lynnmcguire5@gmail.com> - 2024-12-01 15:07 -0600
    Re: What is OOP? Ross Finlayson <ross.a.finlayson@gmail.com> - 2024-12-01 13:36 -0800
    Re: What is OOP? Bonita Montero <Bonita.Montero@gmail.com> - 2024-12-02 08:45 +0100
  Re: What is OOP? Michael S <already5chosen@yahoo.com> - 2024-12-01 23:43 +0200
    Re: What is OOP? wij <wyniijj5@gmail.com> - 2024-12-02 09:02 +0800
  Re: What is OOP? Richard Damon <richard@damon-family.org> - 2024-12-01 17:02 -0500
    Re: What is OOP? wij <wyniijj5@gmail.com> - 2024-12-02 08:57 +0800
      Re: What is OOP? Richard Damon <richard@damon-family.org> - 2024-12-02 08:42 -0500
      Re: What is OOP? Isaac Ganoung <inventor500@vivaldi.net> - 2024-12-08 17:56 +0000
        Re: What is OOP? wij <wyniijj5@gmail.com> - 2024-12-09 08:28 +0800
          Re: What is OOP? wij <wyniijj5@gmail.com> - 2024-12-09 09:27 +0800
  Re: What is OOP? "Chris M. Thomasson" <chris.m.thomasson.1@gmail.com> - 2024-12-01 20:11 -0800
    Re: What is OOP? wij <wyniijj5@gmail.com> - 2024-12-02 16:27 +0800
      Re: What is OOP? wij <wyniijj5@gmail.com> - 2024-12-03 20:43 +0800
  Re: What is OOP? Tim Rentsch <tr.17687@z991.linuxsc.com> - 2024-12-01 20:34 -0800
    Re: What is OOP? Michael S <already5chosen@yahoo.com> - 2024-12-02 10:47 +0200
      Re: What is OOP? Tim Rentsch <tr.17687@z991.linuxsc.com> - 2024-12-15 04:24 -0800
        Re: What is OOP? Michael S <already5chosen@yahoo.com> - 2024-12-15 16:33 +0200
          Re: What is OOP? Tim Rentsch <tr.17687@z991.linuxsc.com> - 2024-12-16 23:59 -0800
    Re: What is OOP? wij <wyniijj5@gmail.com> - 2024-12-02 16:49 +0800
      Re: What is OOP? "Chris M. Thomasson" <chris.m.thomasson.1@gmail.com> - 2024-12-02 14:59 -0800
        Re: What is OOP? wij <wyniijj5@gmail.com> - 2024-12-03 18:10 +0800
        Re: What is OOP? wij <wyniijj5@gmail.com> - 2024-12-03 18:38 +0800
          Re: What is OOP? "Chris M. Thomasson" <chris.m.thomasson.1@gmail.com> - 2024-12-03 12:16 -0800
            Re: What is OOP? wij <wyniijj5@gmail.com> - 2024-12-04 08:44 +0800
              Re: What is OOP? "Chris M. Thomasson" <chris.m.thomasson.1@gmail.com> - 2024-12-06 18:16 -0800
                Re: What is OOP? wij <wyniijj5@gmail.com> - 2024-12-08 01:01 +0800
                Re: What is OOP? Ross Finlayson <ross.a.finlayson@gmail.com> - 2024-12-07 10:46 -0800
              Re: What is OOP? "Chris M. Thomasson" <chris.m.thomasson.1@gmail.com> - 2024-12-19 21:15 -0800
                Re: What is OOP? "Chris M. Thomasson" <chris.m.thomasson.1@gmail.com> - 2024-12-19 21:16 -0800
                Re: What is OOP? "Chris M. Thomasson" <chris.m.thomasson.1@gmail.com> - 2024-12-19 21:17 -0800
                Re: What is OOP? "Chris M. Thomasson" <chris.m.thomasson.1@gmail.com> - 2024-12-23 15:59 -0800
    Re: What is OOP? --- The most important aspect of OOP olcott <polcott333@gmail.com> - 2024-12-06 20:40 -0600
      Re: What is OOP? --- The most important aspect of OOP Richard Damon <richard@damon-family.org> - 2024-12-06 21:45 -0500
        Re: What is OOP? --- The most important aspect of OOP olcott <polcott333@gmail.com> - 2024-12-07 14:07 -0600
        Re: What is OOP? --- The most important aspect of OOP Tim Rentsch <tr.17687@z991.linuxsc.com> - 2024-12-09 09:51 -0800
          Re: What is OOP? --- The most important aspect of OOP Ross Finlayson <ross.a.finlayson@gmail.com> - 2024-12-09 17:43 -0800
        Re: What is OOP? --- The most important aspect of OOP Mr Flibble <leigh@i42.co.uk> - 2025-03-01 21:10 +0000
      Re: What is OOP? --- The most important aspect of OOP wij <wyniijj5@gmail.com> - 2024-12-08 00:32 +0800
  Re: What is OOP? Rosario19 <Ros@invalid.invalid> - 2024-12-04 13:14 +0100
    Re: What is OOP? wij <wyniijj5@gmail.com> - 2024-12-04 22:31 +0800
    Re: What is OOP? wij <wyniijj5@gmail.com> - 2024-12-19 10:32 +0800
    Re: What is OOP? Tim Rentsch <tr.17687@z991.linuxsc.com> - 2025-03-17 10:17 -0700
      Re: What is OOP? wij <wyniijj5@gmail.com> - 2025-03-19 04:58 +0800
        Re: What is OOP? wij <wyniijj5@gmail.com> - 2025-03-20 23:04 +0800
      Re: What is OOP? Michael S <already5chosen@yahoo.com> - 2025-03-20 17:37 +0200
        Re: What is OOP? Tim Rentsch <tr.17687@z991.linuxsc.com> - 2025-03-29 13:33 -0700
      Re: What is OOP? Mr Flibble <flibble@reddwarf.jmc.corp> - 2025-03-27 18:23 +0000
        Re: What is OOP? wij <wyniijj5@gmail.com> - 2025-03-29 11:12 +0800
          Re: What is OOP? Mr Flibble <flibble@reddwarf.jmc.corp> - 2025-03-29 05:07 +0000
          Re: What is OOP? Michael S <already5chosen@yahoo.com> - 2025-03-29 20:39 +0300
            Re: What is OOP? Mr Flibble <flibble@reddwarf.jmc.corp> - 2025-03-29 19:03 +0000
        Re: What is OOP? Tim Rentsch <tr.17687@z991.linuxsc.com> - 2025-03-29 13:36 -0700
  Re: What is OOP? wij <wyniijj5@gmail.com> - 2025-09-28 16:02 +0800

csiph-web