人気のタグ：
仮想化 DNSセキュリティ 形式的検証 到達可能性解析 C言語 コンパイラエラー マクロの衝突 Web拡張機能 開発フレームワーク コモドール64 すべてのタグ

より速く、正確なコードを書くための秘密：メンタルコードプルーフ

2025-07-16

この記事では、より速く、正確にコードを書くためのテクニックを紹介します。「オンライン」証明、つまりコーディングの流れを中断することなく、コードの正しさを頭の中で証明する方法です。著者は、コードの単調性の重視、前条件と後条件の活用、不変量の維持、変更の影響範囲の隔離など、このプロセスを支援するいくつかの戦略を詳しく説明しています。再帰関数とデータ構造に対する帰納的推論についても強調されており、「証明アフィニティ」をコード品質の指標として提唱しています。最後に、著者は、数学的な証明の練習を通じて、コード証明能力を向上させることを提案しています。

続きを読む
(the-nerve-blog.ghost.io)
開発 コード証明

Yコンビネータをゼロから焼く：パート1 -不動点コンビネータ

2025-04-09

この記事では、Yコンビネータ、つまり明示的な自己参照なしで関数型言語で再帰を実装する数学的構成について深く掘り下げています。まず不動点について説明し、その後、Yコンビネータの式を段階的に導出し、自己複製メカニズムを説明します。Ωコンビネータの分析を通して、実行時に自己複製することでYコンビネータが無限ネストを回避する方法を示します。また、ラムダ計算と形式システムの概要も簡単に説明し、以降のパートでYコンビネータをより深く理解するための基礎を築きます。

続きを読む
(the-nerve-blog.ghost.io)
開発 Yコンビネータ

ブール代数でラビリンスのゴブリンの謎解き

2025-03-06

この記事では、映画『ラビリンス』の古典的な騎士と悪党の論理パズルをブール代数を使って解く方法を示しています。著者は、Aを答え、Qを質問への正しい答え、Gをゴブリンが嘘をついているかどうかを表す変数を使って問題をモデル化し、A = G⊕Qを導き出します。もう一方のゴブリンの嘘つき属性を巧みに質問に取り入れることで、方程式が簡略化され、解が明らかになります。著者は、形式化されたアプローチがステップを明確にし、形式システムを推論ツールとして使用する有用性を強調しています。

続きを読む
(the-nerve-blog.ghost.io)
その他 ブール代数 論理パズル 形式的手法