Luna Flow
日本語

luna-generic

このマニュアルは Luna-Flow/luna-generic の予定されている v0.4.0 リリースを説明します。

概要

luna-generic は Luna プロジェクト向けに、一般的な代数 trait と標準数値型の既定インスタンスを提供します。

このリリース候補の中心は次の 3 点です。

  • FromNat と FromInteger は、ℕ と ℤ からの一意な準同型を対象側の trait として表します。
  • Integral は ℤ またはその商 ℤ/2^k であり、normalize はその標準写像の切断でなければなりません。
  • lift_to と Section は、代表元の選択を準同型から切り離します。

インストール

moon add Luna-Flow/luna-generic@0.4.0

次に moon.pkg で "Luna-Flow/luna-generic" をインポートします。このパッケージには MoonBit ツールチェーン 0.10 以降（moonc ≥ 0.10）が必要です。

ページ

このリポジトリは src にある一つの MoonBit パッケージで、文書では core と呼びます。その証明書サブシステム Hom と Section には hom として専用のページがあります。

部分チュートリアルAPI設計
core: trait、変換、インスタンスチュートリアルAPI設計
hom: 準同型と切断チュートリアルAPI設計

公開 Trait

  • AddMonoid, MulMonoid
  • AddGroup, MulGroup
  • Semiring、Ring、Field（可換: ab=baab = ba）
  • FromNat, FromInteger
  • Integral, Nat
  • Num
  • 非推奨: NatHomomorphism、IntegralHomomorphism

公開演算と既定型

  • 演算 trait: One, Zero, Inverse, Conjugate
  • 既定数値型: Int, Int16, Int64, UInt, UInt16, UInt64, BigInt, Float, Double

整数モデル

  • Integral は符号付き整数、符号なし整数、および BigInt を対象とします
  • Nat は代表元が非負である整数型を表します: UInt、UInt16、UInt64
  • 固定幅の整数は ℤ/2^k です。FromInteger::from_integer は 2^k を法として簡約します
  • Integral::normalize は値の代表元を BigInt として選び、from_integer(normalize(x)) == x が成り立ちます
  • 符号なし整数インスタンスは Semiring までです

変換

  • FromInteger::from_integer は ℤ からの標準写像です: BigInt では厳密、固定幅の整数では剰余、Float と Double では丸めになります
  • lift_to(x) は代表元へ持ち上げてから対象へ写します。これは関数であり、準同型ではありません
  • NatHomomorphism::from_nat と IntegralHomomorphism::from_integral は非推奨です。FromNat、FromInteger、lift_to を使ってください

一般化された準同型

  • Hom[S, A, B]: シグネチャ S を保存する写像の証明書。Hom::postulate（証明義務を生む）、標準写像 Hom::from_integer、または推論規則によってのみ構築されます
  • Section[S, Q, A]: 持ち上げが商の各類からちょうど一つの代表元を選ぶことの証明書。Section::of_integral は整数型の標準の切断です
  • シグネチャタグ: AddMonoidSig、MulMonoidSig、AddGroupSig、SemiringSig、RingSig
  • 代数辞書 Algebra[S, A]、演算 Op[A]、積型 Prod[A, B]、縮約の証人 Reduct[S, T]
  • Hom::check / Hom::check_by はサンプル上で準同型の法則を厳密・lax・近似の強さで検査します
  • 詳しくは hom API、チュートリアル、設計 を参照

core チュートリアルではこれらの trait に対して小さな総称アルゴリズムを書きます。core APIはエクスポートされるすべての trait とインスタンスを列挙し、core 設計は階層と変換がこの形になっている理由を説明します。

  • はじめての方: core チュートリアル、次に hom チュートリアル を読んでください。
  • ライブラリで使う方: core API と hom API を手元に置いてください。各 trait にはインスタンスが満たすべき法則が載っています。
  • コントリビュートする方: trait を変更したり推論規則を追加したりする前に、二つの設計ページ core と hom を読んでください。

検証

推奨するリリース前チェック:

moon check
moon test