Formal LabMathematics ⇄ Lean
参照

Navigate the formal text

章・問題・解答・用語・文献を横断検索

検索語を入力してください。

    ↑↓ で移動、Enter で開く、Esc で閉じます。

    用語・記法・文献を一覧から探す

    Exercises

    問題一覧

    全268問を章ごとに一覧できます。各問題は、定義の復元、証明、反例、Lean実装、 表現間の翻訳、文献比較を組み合わせています。問題文と使用できる前提は各章末にあります。

    各問題の直後でヒントだけを開けます。解答では問題文を同じ画面に保ち、 問題の要求に応じた証明・計算・反例・Leanコードと照合できます。

    第1部　形式化の基礎

    第1章　型・項・定義・計算

    1. 型判断の構造を復元するヒント解答
    2. 型検査と評価を別の実験として設計するヒント解答
    3. 拒否される定義を判断の不成立として診断するヒント解答

    第2章　関数・適用・合成

    1. 合成の向きを型だけから復元するヒント解答
    2. カリー化と部分適用を実装と判断で区別するヒント解答
    3. 合成の単位則を等式による証明とLean証明で対照するヒント解答

    第3章　帰納型・場合分け・再帰・構造体

    1. 四種類の規則から有限データ型を設計するヒント解答
    2. 場合分けと構造再帰を呼出し関係で見分けるヒント解答
    3. 帰納型の無限と余帰納的観察を混同しないヒント解答

    第4章　非型付きラムダ計算——束縛・代入・簡約

    1. 名前付き項とde Bruijn添字を往復するヒント解答
    2. シフトと代入の不変条件を一段ずつ追うヒント解答
    3. 簡約規則から評価器の探索方針を分離するヒント解答

    第5章　宇宙階層と宇宙多相

    1. コロンの連鎖を三つの判断へ戻すヒント解答
    2. 宇宙変数が一つでは足りない定義を診断するヒント解答
    3. `max` と `imax` を仕様から読み、具体例へ適用するヒント解答

    第2部　命題と証明

    第6章　命題・証明・含意

    1. 命題とその証明を異なるsortの対象として読むヒント解答
    2. tactic状態をラムダ抽象と関数適用へ戻すヒント解答
    3. 爆発原理の仮定を隠さずに追跡するヒント解答

    第7章　命題論理と構成的・古典的推論

    1. 導入規則と除去規則から証明の情報流を作るヒント解答
    2. 分配則を導出木とLeanの場合分けで二重に記述するヒント解答
    3. 古典原理を使った一点だけを定理の仮定へ抽出するヒント解答

    第8章　述語・全称量化・存在量化

    1. 全称量化を依存する関数として追跡するヒント解答
    2. 存在証明の証人を保存して性質だけを変換するヒント解答
    3. 量化子の順序と限定量化の論理形を反例で固定するヒント解答

    第9章　等式・代入・外延性・一意存在

    1. 等式除去を置き換えの原理として展開するヒント解答
    2. 定義的等しさと外延性の役割分担を証明の各段で指すヒント解答
    3. 存在と一意存在が持つ証拠の成分を分解するヒント解答

    第10章　自然演繹・シーケント計算・証明の正規化

    1. 一つの含意証明を三表現で再構成するヒント解答
    2. 正規化前後で結論と仮定を保存するヒント解答
    3. cutの便利さと除去可能性を区別するヒント解答

    第3部　型付き計算の理論

    第11章　単純型付きラムダ計算——型判断を規則として読む

    1. 証明項を型導出木へ戻すヒント解答
    2. 型の付く項と付かない項の境界を探るヒント解答
    3. 型安全性の三つの主張を分けるヒント解答

    第12章　弱化・交換・縮約・代入

    1. 四つの変換を導出木として復元するヒント解答
    2. ラムダの下の代入を一段ずつ追跡するヒント解答
    3. 構造規則を制限した体系を比較するヒント解答

    第13章　操作的意味論・一段簡約・評価戦略

    1. 一つの評価列を二つの表現で追うヒント解答
    2. 名前呼びと値呼びの停止挙動を分離するヒント解答
    3. 関係と実行関数の対応を証明するヒント解答

    第14章　再帰型・fold/unfold・型の無限展開

    1. 再帰リストを一層ずつ型付けするヒント解答
    2. 型置換の変数捕獲を反例から調べるヒント解答
    3. isoとequiの型付け導出を翻訳するヒント解答

    第15章　保存・進行・型安全性

    1. 進行証明の全分岐を導出木へ戻すヒント解答
    2. 外在的な保存定理を復元するヒント解答
    3. 言語拡張が壊す箇所を診断するヒント解答

    第16章　正規形・弱正規化・強正規化

    1. 三種類の停止主張を反例で分けるヒント解答
    2. 計算可能性述語の関数型場合を読むヒント解答
    3. 正規化器から等式判定器までの欠落を埋めるヒント解答

    第17章　System Fとインプレディカティブ多相

    1. 型抽象の下で二つの添字を追うヒント解答
    2. 多相関数を三つの型へ特殊化するヒント解答
    3. 一様性が型付けだけから読めるか検討するヒント解答

    第18章　論理関係と基本補題

    1. 三つの関係を関数型へ持ち上げるヒント解答
    2. 基本補題の抽象場合を導出するヒント解答
    3. 単項と二項の論理関係を比較するヒント解答

    第19章　パラメトリシティとfree theorem

    1. グラフ関係からfree theoremを導出するヒント解答
    2. 一点関係の左右を変えて恒等性を再証明するヒント解答
    3. 効果がfree theoremを変える反例を作るヒント解答

    第4部　数学の基本言語

    第20章　集合を述語として読む

    1. 集合演算を論理式へ翻訳するヒント解答
    2. 外延性が重ねて使われる箇所を追うヒント解答
    3. 補集合と古典論理の境目を特定するヒント解答

    第21章　数学的関数とその性質

    1. 左逆から単射を復元するヒント解答
    2. 像と逆像の量化を比較するヒント解答
    3. 逆関数を選ぶために必要な仮定を調べるヒント解答

    第22章　関係・同値・順序

    1. 対称性と反対称性を反例で分けるヒント解答
    2. 関数の核関係を証明するヒント解答
    3. 同値関係から商へ進む理由を説明するヒント解答

    第23章　自然数の再帰・場合分け・帰納法

    1. 帰納法の四つの役割を分離するヒント解答
    2. 再帰計算と帰納証明を同じ構造から読むヒント解答
    3. 別の帰納型へ原理を移すヒント解答

    第24章　順序・上限・下限・極大原理

    1. 上限の二条件を別々に検査するヒント解答
    2. 最大と極大の差を有限半順序で可視化するヒント解答
    3. Zornの仮定を有限性で弱めてはならない理由を述べるヒント解答

    第25章　有限性・可算性・基数・無限

    1. 単射・全射・全単射で三種類の比較を作るヒント解答
    2. 対角線証明を表として追跡するヒント解答
    3. 可算性と宇宙を別々の判断へ戻すヒント解答

    第5部　再帰・不動点・無限

    第26章　整礎関係・整礎帰納法・停止する一般再帰

    1. 測度を設計して再帰呼出しを検査するヒント解答
    2. 接近可能性から帰納原理を展開するヒント解答
    3. 互除法の停止性と正しさを分離するヒント解答

    第27章　束・完備格子・単調作用素

    1. 二項演算から普遍性を復元するヒント解答
    2. 空族を含む任意上限・下限を計算するヒント解答
    3. 作用素の単調性を正例と反例で判定するヒント解答

    第28章　最小・最大不動点とKnaster–Tarski定理

    1. 最小不動点証明の二度の単調性を追うヒント解答
    2. 帰納的生成を別の規則へ移すヒント解答
    3. 最大不動点を直接に特徴づけるヒント解答

    第29章　最大不動点・余帰納的述語・双模倣

    1. 常時安全性を有限観察へ展開するヒント解答
    2. 余帰納不変量を小さく選ぶヒント解答
    3. 双模倣と単なる観察一致を分けるヒント解答

    第30章　領域理論・連続写像・再帰方程式

    1. 反復列の上限が固定される証明を分解するヒント解答
    2. 平坦順序のω鎖を分類するヒント解答
    3. 燃料近似を意味論的近似へ接続するヒント解答

    第6部　依存型と型システム

    第31章　型族・依存関数型・依存対型

    1. 定数族から通常の関数と対を復元するヒント解答
    2. 依存対を作り、添字に沿って除去するヒント解答
    3. 論理的存在と計算データを比較するヒント解答

    第32章　同一性型・輸送・外延性原理

    1. `J` から対称性と推移性を再構成するヒント解答
    2. ベクトルの長さ等式に沿って輸送するヒント解答
    3. 四つの外延性原理を比較するヒント解答

    第33章　純粋型システム・ラムダ・キューブ・構成計算

    1. PTSの規則から依存の許可範囲を読むヒント解答
    2. ラムダ・キューブを暗記せず復元するヒント解答
    3. 体系の規則とメタ定理を切り分けるヒント解答

    第34章　部分型と篩型

    1. 値と性質を一つの項として構成するヒント解答
    2. 検査から精密な型へ移すヒント解答
    3. 三つの精密化表現と研究史を比較するヒント解答

    第35章　添字付き帰納族

    1. 構成子の結果型から不可能な場合を読むヒント解答
    2. 添字保存をプログラムの型で検査するヒント解答
    3. 帰納族と部分型による表現を比較するヒント解答

    第36章　一般帰納族・除去規則・厳密正値性

    1. `Expr` の除去原理を規則から復元するヒント解答
    2. 名前変更と環境評価の可換性を証明するヒント解答
    3. 正値性の境界例を分類するヒント解答

    第37章　W型・整礎木・多項式的帰納型

    1. 形と位置から三種類の木を設計するヒント解答
    2. Wリストと通常のリストを往復するヒント解答
    3. foldを始代数の主張へ翻訳する準備をするヒント解答

    第38章　高次同一性・一価性・ホモトピー型理論

    1. 逆写像からファイバーの収縮を再構成するヒント解答
    2. 一価性の主張を三つの弱い主張と比較するヒント解答
    3. 円周の除去原理に必要なデータを特定するヒント解答

    第39章　商型とwell-definedness

    1. 関係を新しい等式へ送るヒント解答
    2. 代表元に依存しない関数を設計するヒント解答
    3. 部分型と商型が捨てるものを対照するヒント解答

    第40章　法則を持つ構造と型クラス探索

    1. 構造のデータと法則を読み分けるヒント解答
    2. 省略された辞書を展開するヒント解答
    3. インスタンス設計の曖昧さを診断するヒント解答

    第41章　型推論・単一化・双方向型付け

    1. 制約生成を導出木と実行結果で照合するヒント解答
    2. 単一化の不変条件と失敗を分類するヒント解答
    3. 合成と検査の境目を設計するヒント解答

    第7部　圏論と普遍性

    第42章　始対象と終対象——零項の普遍性

    1. 存在一意性を型のデータへ分解するヒント解答
    2. 普遍対象の一意性を導くヒント解答
    3. 射を反転して終性を復元するヒント解答

    第43章　積の普遍性

    1. 錐から媒介射を構成するヒント解答
    2. 普遍性をhom集合の同値として読むヒント解答
    3. 零項の積と一意性の意味を調べるヒント解答

    第44章　余積と双対性

    1. 余錐から媒介射を構成するヒント解答
    2. 普遍性を写像集合の同値として表すヒント解答
    3. 双対化を定義から実行するヒント解答

    第45章　圏・射・反対圏・宇宙

    1. 圏の法則を型の整合から検査するヒント解答
    2. 別のモノイドから一対象圏を構成するヒント解答
    3. 反対圏で定理を双対化するヒント解答

    第46章　関手——圏の構造を保つ写像

    1. 保存則を準同型の法則へ翻訳するヒント解答
    2. 合成関手の法則を成分ごとに復元するヒント解答
    3. 反変性を反対圏の型として検査するヒント解答

    第47章　自然変換と関手圏

    1. 可換正方形を型から再構成するヒント解答
    2. 一対象圏で自然変換の存在を判定するヒント解答
    3. 関手圏の圏法則を成分で証明するヒント解答

    第48章　同型・自然同型・圏同値

    1. 片側逆と同型を区別するヒント解答
    2. 自然同型の逆が自然であることを追うヒント解答
    3. 圏同値の判定条件を往復するヒント解答

    第49章　図式・錐・極限・余極限

    1. 積を離散二点図式の極限として復元するヒント解答
    2. 二つの極限を結ぶ同型を構成するヒント解答
    3. 引戻しと押出しを双対化するヒント解答

    第50章　hom関手・普遍元・表現可能関手

    1. hom関手の法則を合成律へ還元するヒント解答
    2. 普遍元から自然な全単射を復元するヒント解答
    3. 積の普遍性を表現可能性へ翻訳するヒント解答

    第51章　米田の補題と米田埋め込み

    1. 米田の全単射の逆法則を証明するヒント解答
    2. 完全忠実性を米田の補題から導くヒント解答
    3. 自然同型から対象同型を回収するヒント解答

    第52章　随伴——homの自然同型・単位・余単位

    1. hom全単射から単位と余単位を取り出すヒント解答
    2. 単位・余単位から転置を復元するヒント解答
    3. 自由・忘却随伴を具体的に読むヒント解答

    第53章　モナド・余モナド・Kleisli圏・Eilenberg–Moore圏

    1. Optionの自然性まで証明するヒント解答
    2. Kleisli合成の圏法則を導くヒント解答
    3. 二つの標準圏を比較するヒント解答

    第54章　自己関手の代数と代数準同型

    1. Option代数の準同型条件を特徴づけるヒント解答
    2. 二項木の一層関手を構成するヒント解答
    3. 代数準同型の合成を検査するヒント解答

    第55章　始代数・fold・Lambekの補題

    1. foldの一意性を可換正方形から再構成するヒント解答
    2. Lambekの補題を始性だけから証明するヒント解答
    3. 不動点と始代数を分ける反例を探すヒント解答

    第56章　自己関手の余代数と余代数準同型

    1. 停止し得る遷移の準同型を作るヒント解答
    2. 余代数準同型の合成を証明するヒント解答
    3. 代数の定義を反対圏で双対化するヒント解答

    第57章　終余代数・anamorphism・振舞意味論

    1. 状態機械からストリームを生成するヒント解答
    2. anamorphismの一意性を証明するヒント解答
    3. 双模倣からストリーム等式を導くヒント解答

    第58章　前層――局所データを制限する反変関手

    1. 制限の合成則を二つの記法で導くヒント解答
    2. 対象ごとの写像を自然変換へ昇格するヒント解答
    3. 定値前層が層にならない状況を分析するヒント解答

    第59章　篩・Grothendieck位相・サイト

    1. 主篩の普遍性を証明するヒント解答
    2. 引戻し公理の合成安定性を証明するヒント解答
    3. 三公理から上方閉性を導くヒント解答

    第60章　層条件・貼り合わせ・層化

    1. 整合族と貼り合わせを定義から判定するヒント解答
    2. 分離的だが層でない前層を構成するヒント解答
    3. 層化の普遍性から一意性を導くヒント解答

    第61章　比較関手・モナド性・Beckの定理

    1. 比較関手の代数法則を三角恒等式へ還元するヒント解答
    2. 三障害を具体例で分類するヒント解答
    3. Beckの仮定から擬逆の構成を追うヒント解答

    第62章　end・coend・双自然性

    1. 自然変換をendの要素へ翻訳するヒント解答
    2. 一対象圏で不変量と余不変量を比較するヒント解答
    3. co-Yoneda公式の商関係を検査するヒント解答

    第63章　Kan拡張——関手の普遍的な延長

    1. 左右の普遍性を射の向きから再構成するヒント解答
    2. 半順序の包含に沿う各点値を計算するヒント解答
    3. 各点公式から射作用を構成するヒント解答
    4. coend公式の生成関係をコンマ圏と照合するヒント解答

    第64章　モノイダル圏——テンソル積と整合性

    1. `Type` の五角形を要素ごとに証明するヒント解答
    2. 単位対象と終対象の違いを説明するヒント解答
    3. 対象対応だけではモノイダル構造にならない理由を示すヒント解答
    4. 整合性定理の適用範囲を判定するヒント解答

    第65章　豊穣圏——hom集合を構造ある対象へ置き換える

    1. `Type`-豊穣圏の三法則を通常の圏法則へ戻すヒント解答
    2. 前順序を真理値豊穣化として構成するヒント解答
    3. Lawvere距離の向きを三角不等式から決定するヒント解答
    4. 自然変換型とhom対象の存在を分離するヒント解答

    第8部　型・計算・圏を結ぶ

    第66章　帰納型・帰納法・始代数——三つの生成原理を接続する

    1. 再帰子から始代数性を再構成するヒント解答
    2. 全空間による依存帰納を計算するヒント解答
    3. 不動点・代数・始代数を反例で分けるヒント解答
    4. 一般圏で不足する構造を特定するヒント解答

    第67章　W型・多項式関手・自由代数——形と位置から帰納構造を作る

    1. 自然数とリストの多項式を回収するヒント解答
    2. W型の始性証明を可換図式から再構成するヒント解答
    3. 自由代数の二つの普遍性を往復するヒント解答
    4. 多項式ではない厳密正値関手との境界を調べるヒント解答

    第68章　余帰納法・双模倣・最大不動点・終余代数——関係と振舞いを接続する

    1. 双模倣からストリーム等式までの二種類の帰納を分けるヒント解答
    2. 異なる内部状態表現の機械を比較するヒント解答
    3. 終余代数への核関係が後不動点になる理由を一般化するヒント解答
    4. 最大不動点・不動点同型・終性の反例を整理するヒント解答

    第69章　無限の三つの意味——基数・尽きない観察・無限図式

    1. 状態数と振舞い数の四つの組合せを作るヒント解答
    2. 有限prefixの糸とストリームの同値を完成するヒント解答
    3. 一般の錐として可算逆極限を再構成するヒント解答
    4. ストリーム全体の基数と一つの観察列を分けるヒント解答

    第70章　デカルト閉圏——積・指数対象・カリー化

    1. 評価射からカリー化の存在一意性を再構成するヒント解答
    2. β則・η則・三角恒等式を対応させるヒント解答
    3. 指数対象を表現可能性として構成するヒント解答
    4. デカルト閉圏とモノイダル閉圏の差を射で検査するヒント解答

    第71章　単純型付きラムダ計算の圏論的意味論——判断を射へ移す

    1. 全ての構文的代入について意味論的置換補題を証明するヒント解答
    2. β・η以外の等式をモデルで検査するヒント解答
    3. 構文圏の対象・射・合成を設計するヒント解答
    4. 構造規則が意味射のどこに現れるかを追跡するヒント解答

    第72章　スライス圏・添字圏・ファイブレーション——変化する文脈の上で対象を運ぶ

    1. `Type` の引戻しの普遍性を同値としてまとめるヒント解答
    2. スライス圏の射を手で合成するヒント解答
    3. 二回の再添字付けを一回の再添字付けと比較するヒント解答
    4. Cartesian持ち上げの一意性を図式で証明するヒント解答
    5. Grothendieck構成の射を依存対として読むヒント解答

    第73章　局所デカルト閉圏——依存積を再添字付けの右随伴として捉える

    1. 二つの型族随伴の自然性を証明するヒント解答
    2. 空ファイバーと多元ファイバーで依存積を計算するヒント解答
    3. 通常のカリー化を依存カリー化から回収するヒント解答
    4. 合成に沿う依存積の比較同型を追跡するヒント解答
    5. 局所デカルト閉性の二つの定義を結ぶヒント解答

    第74章　依存型理論の圏論的意味論——文脈・型・項・代入を再構成する

    1. `Type` モデルをcategory with familiesの法則として整理するヒント解答
    2. 項と表示射の切断の同値を証明するヒント解答
    3. 依存積のβη則を随伴の三角恒等式へ翻訳するヒント解答
    4. 置換のcoherence問題を具体例で示すヒント解答
    5. 外延的同一性型と内包的同一性型を分離するヒント解答
    6. 構文モデルの初期性を正確に述べるヒント解答

    第75章　モノイダル閉圏——内部hom・評価・自己豊穣化

    1. 評価射からhom同値の一意性を再構成するヒント解答
    2. 内部カリー化同型の二重評価を追跡するヒント解答
    3. 内部合成から通常の射の合成を回収するヒント解答
    4. デカルト構造が弱化と縮約を生むことを示すヒント解答
    5. 組紐によって左右の閉性を移すヒント解答
    6. 左随伴としてのテンソルが余極限を保つことを導くヒント解答

    第76章　線形論理・線形型——仮定を資源として追跡する

    1. 弱化と縮約が導出をどこで止めるか調べるヒント解答
    2. β簡約が資源使用を保存する条件を示すヒント解答
    3. シーケント規則を圏の射へ逐語的に翻訳するヒント解答
    4. 乗法的結合子と加法的結合子を反例で分けるヒント解答
    5. 余モナドと線形指数余モナドの差を列挙するヒント解答
    6. LNL随伴から指数様相を構成するヒント解答

    第77章　モナドと計算効果——値から計算を分離して合成する

    1. 三つの具体モナドを同じ法則で比較するヒント解答
    2. 値呼び適用の表示をstrengthから構成するヒント解答
    3. ChoiceTreeの自由性を証明するヒント解答
    4. 例外ハンドラをEilenberg–Moore代数として調べるヒント解答
    5. 効果の層順序を状態と例外で比較するヒント解答
    6. 表示の健全性とadequacyを分けるヒント解答

    第78章　トポスと圏論的論理——部分対象を真理値で分類する

    1. `Type` の単射から特性述語を構成するヒント解答
    2. 分類子と表現可能性の二方向を再構成するヒント解答
    3. 前層の特性篩を要素ごとに計算するヒント解答
    4. 冪対象の所属関係から部分対象族を回収するヒント解答
    5. 排中律が失敗する局所的な真理値を調べるヒント解答
    6. 二種類のトポスと保存される論理を比較するヒント解答

    第79章　再帰型の意味論——構文・近似・関手不動点を接続する

    1. 始鎖の最初の五段階を完全に記述するヒント解答
    2. 不動点同型から始性が従わない反例を強化するヒント解答
    3. `1+X` の終解に無限要素を加えるヒント解答
    4. 負の再帰出現の向きを型で追跡するヒント解答
    5. 有限燃料とKleene反復を接続するヒント解答
    6. 操作的意味論と表示的意味論の境界を監査するヒント解答