25/03/08 08:33:14.12 3yKaxuFZ.net
思い付きとは？
9:１３２人目の素数さん
25/03/08 10:19:37.00 lUzSDHir.net
たとえばFizzBuzzのプログラムが「正しい」ことはどうやって証明するのか
入力が固定なら、出力を正解と差分比較すればいいが
10:１３２人目の素数さん
25/03/08 10:32:47.02 3yKaxuFZ.net
プログラムが仕様通り作られていることを形式的に証明する、のか
11:１３２人目の素数さん
25/03/08 10:33:31.33 3yKaxuFZ.net
ホーア論理
12:１３２人目の素数さん
25/03/08 10:34:11.32 3yKaxuFZ.net
ダイクストラのプログラム検証法
13:１３２人目の素数さん
25/03/08 10:36:11.90 3yKaxuFZ.net
coq
14:１３２人目の素数さん
25/03/08 12:20:00.49 0f9oMeD6.net
>>9
自然数が
・3の倍数だが5の倍数ではない
・5の倍数だが3の倍数ではない
・3の倍数かつ5の倍数
・それ以外
の無縁和に分かれることの証明を表現する
それぞれのケースに対する関数を定義する
FizzBuzzの上限と下限を決める
このようになっていれば形式的に証明できると思う
15:poem
25/03/09 18:57:21.39 HM1Gkwqb.net
ｽﾚﾘﾝｸ(math板:44番)-46/
16:１３２人目の素数さん
25/03/10 06:51:19.10 9N9g1qmV.net
そもそもね、仕様書がプログラミング通り
作られてるかな❓
て、ゆうか、FizzBuzzの仕様書？の方が意味不明
プログラミング言語の記述の方が分かりやすい
てか、
if (n%15) console.log(FizzBuzz);
else if (n%3) console.log(Fizz);
ホゲホゲ
てプログラミング結果と一致するか
ま、nが1〜300位までチェックすりゃ大丈夫だろ
て、ゆぅかっ、1,2,3,5,15,16 の６通りで
いいぢゃーーーん。
てか、予算は幾らあるの❓
そりゃさ、自然数は可算∞個あるのだから
可算無限個とおりチェックしなさーーーい
ま、ポクは、６通りチェックするだけで
非可算無限チェックしたのと同じ
位、それがバッチリか検証できる超能力を
有するウチュ〰人だよぉーーー
17:16 怪しい呟き
25/03/10 06:56:50.93 9N9g1qmV.net
console.log(FizzBuzz); 🐴🦌だねぇー
console.log("FizzBuzz"); だろ
ちみは、15の倍数とか、任意の自然数のとき、
定義されてませーーーんとか答えると
正確なのか？。ちゃんと検証してから投稿しなさーーーい
by 自分へ返答、変答、変な解答、怪解でした。(;_;)/~~~
18:16は、知能は、ヤバイ(自演)
25/03/11 10:57:04.40 3Bh/sPXv.net
>>16 よ。チミは、昨日の自分ぢゃーん
そもそも、
15の倍数⇒3の倍数∧5の倍数 だから
15とか30とか45とかは、
FIZZ も BUZZ もドッチも正解だぁ
FIZZ、BUZZが正解でも正解たけどさ、
FIZZ でも 正解にしてあげて、
てか、国語なら必要条件さえ答えれば
💯なのに、数学は零点になるよな❓
てか、地球人のルールの解説ヤバイ
19:poem
25/03/11 12:22:09.43 7G9/jMlG.net
39 ご冗談でしょう？名無しさん 225/03/11(火) 10:33:16.84
部品は高尚な概念なんだよ
部品はブリコラージュ（器用仕事）の上位互換
エントロピー、オキシトシン、アルファ波などを組み込むと機械という高尚な概念になる
大部分は唯物論の実証や数学から来ているがシャノンエントロピーなんて例外もある
41 poem 225/03/11(火) 12:10:33.57
シャノンエントロピーと調べたら
2進数情報量？
10進数情報量が
ハートレーエントロピーと言ったり？
42 poem 225/03/11(火) 12:14:35.95
念の為に言うけど
同じ5MBの情報量でも
情報の入れ子具合で
機能の水準が違うからね
1,0の入れ子(括弧で括り)無しだと単なるバイナリで情報表現は1次元紐の水準しかなく
入れ子ありだと2次元3次元n次元以上の情報表現になる
だから2進数情報量だけでは機能水準を表していない
43 poem 225/03/11(火) 12:15:49.05
単なるエントロピーつまり乱雑さに
入れ子とかあるのかは知らない
44 poem 225/03/11(火) 12:16:18.57
熱力学のエントロピーの方ね
20:１３２人目の素数さん
25/03/11 17:06:43.45 LeJDstie.net
哲学で実証の証明をやってる
全体は部分の総和という理論
メソッド理論の観点から見た心理学の実証
心理学は神経科学により実証される
神経科学（オキシトシン）や脳科学（アルファ波）がメソッド主義であり
数的関係を持つ部品になる
この部品こそ研鑽の集大成でありタイプ理論などは机上の空論であり部品たり得ない
全体は部分（部品）の総和であるべきである
ｽﾚﾘﾝｸ(psycho板:21番)
21:16
25/03/13 04:08:42.01 1QPgiK/Y.net
３日前の自分、壱拾六へ
FIZZ BUZZのルールの地球人よる説明も
カナリ、あれだけどさ、
地球人が発明した閏年の説明も
カナリ。あれだな。
西暦年が4で割切れるは、閏年。でも
西暦年が100で割切れるは、平年。でも
西暦年が400で割切れるは、閏年。
としてるよう、ぢゃ。ぢゃから
地球人は、おそらく、絶対
400の倍数は、100の倍数ぢゃない、かつ
100の倍数は、4の倍数ぢゃない。
と、理解してるのか❓
全く数学というか算数すらもダメな地球人
てか、西暦2000年は、閏年でバグちゃう
バグが、発生しちゃったようだぜ。
by 👾の感想文でした。(^.^)/~~~
22:16
25/03/13 04:16:37.06 1QPgiK/Y.net
でもさ、ちょう安易に、
「西暦は、４で割り切れるは、閏年」
なんてしてるロジックは、西暦2000年問題は、クリア
🐴🦌な奴が開発したロジックがバグらんって
地球の自転速度てか公転速度を決めた神サマは、
カナリ、チョー天才だな。by 👾
23:１３２人目の素数さん
25/03/26 10:12:32.43 RyqxVhEy.net
むしろプログラムこそが証明なんだが
24:１３２人目の素数さん
25/03/29 10:38:37.99 sWaetczbH
何もかも支離滅裂で突っ込むのもウンザリな齋藤鉄夫だの竹谷とし子だの強盗殺人推進公明党か゛カンコー立国た゛のほざいてJALた゛のANＡだの
クソポリヘリた゛のテ囗リストに莫大な温室効果ガスまき散らさせて気候変動、災害連発させて人殺しまくっていなか゛ら気候変動対策だの
防災だの平然と嘘八百ほざいて憲法1З条2５条2９条とガン無視で力による一方的な現状変更によって閑静な住宅地まで騒音まみれ
知的産業根絶やしにして国際競爭力壞滅させて子の学習環境破壊して私腹を肥やしていながら闇バイトは無差別強盗で卑劣．強盗殺人は俺らの
専売特許だからなとか寝言は寝てから言えやインバウンド何兆円だのほざきながら ─千億とか補助金出してるあたりで気づくへ゛きだか゛
カンコーこそが国民貧困化の根源、流出する石油代や農作物その他の被害など物価高騰引き起こしたり何年もカンコーだのほざいていなか゛ら
儲かってるのは癒着業者だけ国民不倫民主党の戯言とかどうでもいいが犯罪惹起して税金泥棒してるクソポリ公から惡質おもちゃ取り上げて
航空燃料税リッター１万円にするた゛けて゛もくだらない扶養云々全廃して公平な最低所得保障財源で治安回復するわ
(rｅf.］ ＴTps:/／www.call4.jp/info.рhp?tУpe=items&id＝I０00006２
URLﾘﾝｸ(haneda-proj)<)Ｃom／
ttＰs://n-souonhigaisosУoudan.amebaownd.com／
25:１３２人目の素数さん
25/09/28 21:25:49.58 ukWFqdUB.net
>>1
任意のプログラムコードをHaskellに変換する。
Haskellコードを数学に置き換えて証明する（ここは手動。HaskellからTeXへの変換手段があれば自動化できそう）
26:１３２人目の素数さん
25/10/19 14:15:30.82 iXLntZwi.net
プログラムのいったい何を証明したいのか意味不明
プログラムが何かの証明を記述しているのだろうと思えば>>23
プログラムの正しさを証明したいのだとすればホーアロジック
etc
27:１３２人目の素数さん
25/10/19 14:56:09.71 4oiu/XMI.net
>>23
その場合、バグとは証明すべき定理を取り違えたことで生じる（笑）
28:１３２人目の素数さん
26/01/20 00:23:33.03 HOLWUcLr/
厚木だの横田た゛の何千人もが何度も訴訟やって差止めできす゛弁護士費用で相殺される程度の賠償金で誤魔化すテロ国家に無駄なことしてないで
暴力で解決すること考えろよ基地に色々投げ込んだりレーザ─照射したりニュースにすらならない些細なことはやってるようた゛が
霞が関を灰燼に帰しないと何も解決しないっていい加減学習しろよな民主主義とは民衆による暴力を前提にした社会体制のことをいうんだそ゛
しかも基地周辺の連中の場合引っ越しゃいいものをこいつらのせいでJАLだのANAだのテロリストに海に囲まれた日本でわざわさ゛陸域
クソ航空騒音まみれにさせて安眠妨害に生産性破壊に住民の健康に生業にと壊滅させて被害者はお前らだけじゃねえんだぞみたいな囗実
与えてるだけて゛税金強奪に留まらない害悪を日本中に撤き散らしてるのか゛実態
独立住民投票すらしない沖縄の連中た゛の被爆をネタに寝言ほさ゛いてる連中だのも赤の他人の血税に寄生してるだけなのがバレバレ
莫大な温室効果カ゛スまき散らして気候変動災害連発させて人殺しまくってるクソ航空機廃絶させない連中の行動は全てくだらない茶番
航空機連絡先情報 noise.web.fＣ２.Ｃom