Warning: mysqli::__construct(): (HY000/1203): User howardkn already has more than 'max_user_connections' active connections in D:\Inetpub\vhosts\howardknight.net\al.howardknight.net\includes\artfuncs.php on line 21
Failed to connect to MySQL: (1203) User howardkn already has more than 'max_user_connections' active connectionsPath: eternal-september.org!news.eternal-september.org!.POSTED!not-for-mail From: wij Newsgroups: comp.lang.c++ Subject: Re: What is OOP? Date: Mon, 09 Dec 2024 08:28:51 +0800 Organization: A noiseless patient Spider Lines: 164 Message-ID: <8adbdfc97097af5e53c0a22689362f1af2ae2b93.camel@gmail.com> References: <3a72f45ce7a77c6272e207f009ba09aece96f8df@i2pn2.org> <253c0b3fe3ac8ea661af3347f93529bd0f03f3e2.camel@gmail.com> MIME-Version: 1.0 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable Injection-Date: Mon, 09 Dec 2024 01:28:53 +0100 (CET) Injection-Info: dont-email.me; posting-host="d21130fcf26d215eec62e322955e4662"; logging-data="71871"; mail-complaints-to="abuse@eternal-september.org"; posting-account="U2FsdGVkX19MWAO6OaiEVsN845mQGvHY" User-Agent: Evolution 3.50.2 (3.50.2-1.fc39) Cancel-Lock: sha1:CJ6TGbe++uA4D+X7/2CHkDyJ3+4= In-Reply-To: On Sun, 2024-12-08 at 17:56 +0000, Isaac Ganoung wrote: > On Mon, 02 Dec 2024 08:57:41 +0800, wij wrote: >=20 > > How do you verify correctness just by the program 'logic'? >=20 > You use a functional language like Haskell. You are probably looking for= =20 > 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=C2=A0of 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 #include using namespace Wy; using namespace Sc; #include "Sc/TestRule.inc" // This file must be included after the above us= ing... 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=3D0; ri " << wrd(rule.rule(i).deduct_pattern()) << WY_ENDL; } cout << "-----------------" << WY_ENDL; }; void t0() { Errno r; make_rule(); Search sr0(rule); const DyExpr ini_expr=3Dfac(NatNum_2); const DyExpr des_expr=3DNatNum_2; cout << "Compute: " << wrd(ini_expr) << " -> " << wrd(des_expr) << WY_ENDL= ; if((r=3Dsr0.search(ini_expr,des_expr,10,Search::Mode::Shortest))!=3DOk) { WY_THROW(r); } const Array& garr=3D sr0.gpath(); if(garr.is_empty()) { cout << "goal is not found" WY_ENDL; } else { cout << garr.size() << " steps" WY_ENDL; for(size_t i=3D0; i (_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.