Luna Flow
日本語

hom API

役割

hom サブシステムは一般化された準同型を提供します。Hom[S, A, B] は写像 A -> B で、シグネチャ S のすべての演算を保存するという証明書を伴います。Section[S, Q, A] は、持ち上げが商の各類からちょうど一つの代表元を選ぶことを証明します。どちらの証明書もこのパッケージの外では偽造できません。未証明の葉は Hom::postulate、Section::postulate、および標準の Hom::from_integer と Section::of_integral で、後者二つの義務は trait インスタンスにあります。

ソース: src/hom.mbt、src/section.mbt。数学的な内容は hom 設計 にあります。

このページの例は次の宣言を前提とします:

using @luna-generic {
  type Hom,
  type Section,
  type Algebra,
  type Op,
  type Prod,
  type Reduct,
  type AddMonoidSig,
  type MulMonoidSig,
  type AddGroupSig,
  type SemiringSig,
  type RingSig,
  semiring_to_add_monoid,
  semiring_to_mul_monoid,
  ring_to_semiring,
  ring_to_add_group,
  add_group_to_add_monoid,
}

let ints : Array[Int] = [0, 1, -1, 7, 2147483647, -2147483648]

let longs : Array[Int64] = [0L, 1L, -1L, 7L, 4294967296L, 9223372036854775807L]

シグネチャタグ

シグネチャタグは型レベルにだけ現れる空の列挙型で、Hom、Section、Algebra、Reduct のパラメータ S として使います。利用者が独自に定義することもできます。

AddMonoidSig

AddMonoidSig はシグネチャ 0、+ です。

pub enum AddMonoidSig {
}

MulMonoidSig

MulMonoidSig はシグネチャ 1、* です。

pub enum MulMonoidSig {
}

AddGroupSig

AddGroupSig はシグネチャ 0、+、neg です。

pub enum AddGroupSig {
}

SemiringSig

SemiringSig はシグネチャ 0、1、+、* です。

pub enum SemiringSig {
}

RingSig

RingSig はシグネチャ 0、1、+、*、neg です。

pub enum RingSig {
}

代数辞書

同じ S の二つの辞書は、同じ演算（名前とアリティ）を同じ順序で並べる必要があります。そうでない場合 Algebra::prod と Hom::check_by は abort します。

証明書は台集合ごとに S-代数が一つだけであることを前提とします。同じ台集合上の同じ S の辞書は、すべて演算を同じように解釈しなければなりません。then は中間の台集合を経由して合成するため、そこに異なる Algebra::make 辞書が二つあると、合成した写像はどちらも保存しません。

Op

Op[A] は単一ソートのシグネチャの一つの演算です。

pub(all) struct Op[A] {
  name : String
  arity : Int
  eval : (Array[A]) -> A
}

arity == 0 は定数です。eval はちょうど arity 個の引数を受け取ります。

Algebra

Algebra[S, A] はキャリア A 上でのシグネチャ S の解釈で、シグネチャが定める順に並べた Op[A] のリストです。

pub struct Algebra[S, A] {
  // private fields
}

Algebra::make

Algebra::make(ops) は独自シグネチャタグ用の辞書を作ります。

pub fn[S, A] Algebra::make(Array[Op[A]]) -> Algebra[S, A]

上で説明したとおり、タグとキャリアの組ごとに辞書は一つにします。

enum MaxSig {}

fn max_int() -> Algebra[MaxSig, Int] {
  Algebra::make([
    Op::{ name: "max", arity: 2, eval: xs => if xs[0] > xs[1] { xs[0] } else { xs[1] } },
  ])
}

Algebra::add_monoid, Algebra::mul_monoid, Algebra::add_group, Algebra::semiring, Algebra::ring

これらの関数は、A の構造 trait インスタンスから組み込みタグの辞書を導きます。

pub fn[A : AddMonoid] Algebra::add_monoid() -> Algebra[AddMonoidSig, A]
pub fn[A : MulMonoid] Algebra::mul_monoid() -> Algebra[MulMonoidSig, A]
pub fn[A : AddGroup] Algebra::add_group() -> Algebra[AddGroupSig, A]
pub fn[A : Semiring] Algebra::semiring() -> Algebra[SemiringSig, A]
pub fn[A : Ring] Algebra::ring() -> Algebra[RingSig, A]

演算はタグの順に並びます。たとえば RingSig では 0、1、+、*、neg です。trait の一貫性により、タグとキャリアの組ごとに辞書は一つになります。

test "built-in dictionaries" {
  let int_ring : Algebra[RingSig, Int] = Algebra::ring()
  let id : Hom[RingSig, Int, Int] = Hom::id()
  assert_true(id.check(int_ring, int_ring, ints))
}

Algebra::prod

Algebra::prod(a, b) は Prod[A, B] 上の成分ごとの積代数です。

pub fn[S, A, B] Algebra::prod(Algebra[S, A], Algebra[S, B]) -> Algebra[S, Prod[A, B]]

各演算は fst には a で、snd には b で作用します。a と b の演算の並びが一致しないと中断します。

積型

Prod

Prod[A, B] はフィールド fst と snd を持つ二項積のキャリアです。

pub(all) struct Prod[A, B] {
  fst : A
  snd : B
} derive(Eq, @debug.Debug)

演算は成分ごとに行います。Prod は Add、Mul、Neg、Sub、Zero、One を実装し、両成分が実装していれば AddMonoid、MulMonoid、AddGroup、Semiring、Ring も実装します。

Prod::add, Prod::sub, Prod::mul, Prod::neg, Prod::zero, Prod::one

これらのメソッドは成分ごとの演算で、+、-、*、単項 -、Zero / One trait としても使えます。

pub fn[A : Add, B : Add] Prod::add(Prod[A, B], Prod[A, B]) -> Prod[A, B]
pub fn[A : Sub, B : Sub] Prod::sub(Prod[A, B], Prod[A, B]) -> Prod[A, B]
pub fn[A : Mul, B : Mul] Prod::mul(Prod[A, B], Prod[A, B]) -> Prod[A, B]
pub fn[A : Neg, B : Neg] Prod::neg(Prod[A, B]) -> Prod[A, B]
pub fn[A : Zero, B : Zero] Prod::zero() -> Prod[A, B]
pub fn[A : One, B : One] Prod::one() -> Prod[A, B]
(a,b)+(a′,b′)=(a+a′,b+b′),(a,b)(a′,b′)=(aa′,bb′),0=(0,0),1=(1,1).(a, b) + (a', b') = (a + a', b + b'), \qquad (a, b)(a', b') = (aa', bb'), \qquad 0 = (0, 0), \qquad 1 = (1, 1).

Prod::equal, Prod::not_equal, Prod::to_repr

これらのメソッドは成分ごとに比較し、デバッグ用に Prod を表示します。新しいコードでは ==、!=、inspect を使ってください。

pub fn[A : Eq, B : Eq] Prod::equal(Prod[A, B], Prod[A, B]) -> Bool
pub fn[A : Eq, B : Eq] Prod::not_equal(Prod[A, B], Prod[A, B]) -> Bool
pub fn[A : @debug.Debug, B : @debug.Debug] Prod::to_repr(Prod[A, B]) -> @debug.Repr
test "prod" {
  let p : Prod[Int, Double] = { fst: 2, snd: 0.5 }
  let q : Prod[Int, Double] = { fst: 3, snd: 4.0 }
  assert_eq(p * q + Prod::one(), { fst: 7, snd: 3.0 })
  assert_true(p != q)
}

準同型

Hom

Hom[S, A, B] は、S のすべての演算を保存すると証明された写像 A -> B です。

pub struct Hom[S, A, B] {
  // private fields
}

証明書の意味は、S の項数 nn の各演算 ω\omega とすべての x1,…,xnx_1, \dots, x_n について次が成り立つことです。

f(ωA(x1,…,xn))=ωB(f(x1),…,f(xn)).f(\omega_A(x_1, \dots, x_n)) = \omega_B(f(x_1), \dots, f(x_n)).

Hom の値を作れるのはこのパッケージだけです。葉は Hom::postulate と Hom::from_integer で、ほかの構成子はすべて推論規則です。

Hom::postulate

Hom::postulate(f) は証明なしで f を S-準同型として信頼し、証明責務を生みます。

pub fn[S, A, B] Hom::postulate((A) -> B) -> Hom[S, A, B]

呼び出し側は、S の各演算 op とすべての引数 xs について f(op_A(xs)) == op_B(xs.map(f)) を約束します。写像を緩い関係や許容誤差で検査するだけの場合でも、約束は常に厳密な等式です。各呼び出しには check テストを添えてください。

fn int64_to_int() -> Hom[RingSig, Int64, Int] {
  Hom::postulate(x => x.to_int())
}

test "postulate and check" {
  assert_true(int64_to_int().check(Algebra::ring(), Algebra::ring(), longs))
}

Hom::apply

h.apply(x) は元の写像を適用します。

pub fn[S, A, B] Hom::apply(Hom[S, A, B], A) -> B
test "apply" {
  inspect(int64_to_int().apply(4294967301L), content="5")
}

Hom::id

Hom::id() は恒等準同型です。

pub fn[S, A] Hom::id() -> Hom[S, A, A]

Hom::then

h.then(g) は合成で、まず h、次に g です。

pub fn[S, A, B, C] Hom::then(Hom[S, A, B], Hom[S, B, C]) -> Hom[S, A, C]

ff と gg が ω\omega を保存するなら、g∘fg \circ f も保存します:

g(f(ω(x)))=g(ω(f(x)))=ω(g(f(x))).g(f(\omega(x))) = g(\omega(f(x))) = \omega(g(f(x))).

Hom::forget

h.forget(r) は Reduct[S, T] の証拠に沿って構造を忘れます。

pub fn[S, T, A, B] Hom::forget(Hom[S, A, B], Reduct[S, T]) -> Hom[T, A, B]

S のすべての演算を保存する写像は、より小さいシグネチャ T の演算も保存します。

Hom::pair, Hom::fst, Hom::snd

Hom::pair(f, g) は x を { fst: f(x), snd: g(x) } に写します。Hom::fst() と Hom::snd() は Prod からの射影です。

pub fn[S, A, B, C] Hom::pair(Hom[S, A, B], Hom[S, A, C]) -> Hom[S, A, Prod[B, C]]
pub fn[S, A, B] Hom::fst() -> Hom[S, Prod[A, B], A]
pub fn[S, A, B] Hom::snd() -> Hom[S, Prod[A, B], B]

これらは pair(f, g).then(fst()) = f と pair(f, g).then(snd()) = g を満たします。

test "composition rules" {
  let h = int64_to_int()
  let low : Hom[RingSig, Int64, Int16] = Hom::postulate(x => Int16::from_int(x.to_int()))
  let p = Hom::pair(h, low)
  let back = p.then(Hom::fst())
  let additive = h.forget(ring_to_add_group)
  inspect(back.apply(4294967301L), content="5")
  assert_true(additive.check(Algebra::add_group(), Algebra::add_group(), longs))
}

Hom::to_add_group

h.to_add_group() は群の間の加法モノイド準同型を加法群準同型に格上げします。

pub fn[A : AddGroup, B : AddGroup] Hom::to_add_group(Hom[AddMonoidSig, A, B]) -> Hom[AddGroupSig, A, B]

新しい責務はありません。f(−x)+f(x)=f(−x+x)=f(0)=0f(-x) + f(x) = f(-x + x) = f(0) = 0 なので f(−x)=−f(x)f(-x) = -f(x) です。

Hom::to_ring

h.to_ring() は環の間の半環準同型を環準同型に格上げします。

pub fn[A : Ring, B : Ring] Hom::to_ring(Hom[SemiringSig, A, B]) -> Hom[RingSig, A, B]

to_add_group と同じ計算により、新しい責務はありません。

Hom::from_integer

Hom::from_integer() は FromInteger の標準写像 ℤ → R を証明書にしたものです。

pub fn[R : FromInteger] Hom::from_integer() -> Hom[SemiringSig, @bigint.BigInt, R]

すべての入力で成り立ちます。R が環なら to_ring で格上げします。Float と Double の対象では丸めの範囲でしか成り立ちません。固定幅のソースは、まず Section::of_integral で持ち上げます。

test "from_integer" {
  let h : Hom[RingSig, BigInt, Int] = Hom::from_integer().to_ring()
  let samples = [0, 1, -1, 2147483647].map(BigInt::from_int)
  assert_true(h.check(Algebra::ring(), Algebra::ring(), samples))
}

切断

切断は、準同型 proj : A -> Q に沿って商 Q を A へ持ち上げるもので、proj(lift(q)) == q を満たします。持ち上げ自体は準同型ではありませんが、proj の核を法としてすべての演算を保存し、結果が代表元であるときは厳密に保存します。

切断の法則は、引数の類から外れる持ち上げを拒否します。ただし代表元の選び方は決めません。[0, 2^32) と [-2^31, 2^31) はどちらも BigInt -> Int の切断ですが、符号付きの順序を保つのは後者だけです。

Section

Section[S, Q, A] は射影 proj : A -> Q に沿って商 Q を A へ持ち上げるものです。

pub struct Section[S, Q, A] {
  // private fields
}
π(s(q))=qfor every q∈Q.\pi(s(q)) = q \quad \text{for every } q \in Q.

Section::postulate

Section::postulate(proj, lift) は lift を proj の切断として信頼し、証明責務を生みます。

pub fn[S, Q, A] Section::postulate(Hom[S, A, Q], (Q) -> A) -> Section[S, Q, A]

呼び出し側はすべての q について proj.apply(lift(q)) == q を約束します。proj は自身の Hom の責務を持ちます。

test "section postulate" {
  let truncate : Hom[RingSig, Int64, Int] = Hom::postulate(x => x.to_int())
  let widen = Section::postulate(truncate, x => x.to_int64())
  assert_true(widen.check(ints))
}

Section::of_integral

Section::of_integral() は整数型の標準の切断です。

pub fn[Z : Integral] Section::of_integral() -> Section[SemiringSig, Z, @bigint.BigInt]

proj は FromInteger::from_integer、lift は Integral::normalize です。責務はこれらのインスタンスにあります。Z が環なら to_ring を使います。

Section::lift, Section::proj

s.lift(q) は q の選ばれた代表元、s.proj() は商への射影です。

pub fn[S, Q, A] Section::lift(Section[S, Q, A], Q) -> A
pub fn[S, Q, A] Section::proj(Section[S, Q, A]) -> Hom[S, A, Q]

Section::normalize

s.normalize(a) は lift(proj(a))、つまり a の正規形です。

pub fn[S, Q, A] Section::normalize(Section[S, Q, A], A) -> A

二つの値が合同であるのは、正規形が等しいとき、かつそのときに限ります。

Section::is_representative

s.is_representative(a) は a がその類の選ばれた代表元か、つまり normalize(a) == a かを判定します。

pub fn[S, Q, A : Eq] Section::is_representative(Section[S, Q, A], A) -> Bool

そのような結果では、持ち上げは A の演算と完全に一致します。

test "representatives" {
  let s : Section[RingSig, Int, BigInt] = Section::of_integral().to_ring()
  let big = BigInt::from_int64(4294967296L)
  inspect(s.lift(-1), content="-1")
  inspect(s.proj().apply(big + BigInt::from_int(5)), content="5")
  inspect(s.normalize(big + BigInt::from_int(5)), content="5")
  assert_true(s.is_representative(s.lift(7) + s.lift(1)))
  assert_false(s.is_representative(s.lift(2147483647) + s.lift(1)))
}

Section::then

s.then(next) は s で Q を A へ、次に next で A を B へ持ち上げます。

pub fn[S, Q, A, B] Section::then(Section[S, Q, A], Section[S, A, B]) -> Section[S, Q, B]

射影は next.proj の後に s.proj です。新しい責務はありません。s,ts, t を二つの持ち上げ、πs,πt\pi_s, \pi_t をその射影とすると、πs(πt(t(s(q))))=πs(s(q))=q\pi_s(\pi_t(t(s(q)))) = \pi_s(s(q)) = q です。

Section::forget, Section::to_add_group, Section::to_ring

これらの推論規則は射影のシグネチャを変え、持ち上げは変えません。

pub fn[S, T, Q, A] Section::forget(Section[S, Q, A], Reduct[S, T]) -> Section[T, Q, A]
pub fn[Q : AddGroup, A : AddGroup] Section::to_add_group(Section[AddMonoidSig, Q, A]) -> Section[AddGroupSig, Q, A]
pub fn[Q : Ring, A : Ring] Section::to_ring(Section[SemiringSig, Q, A]) -> Section[RingSig, Q, A]

それぞれ Hom::forget、Hom::to_add_group、Hom::to_ring に従います。

Section::check

s.check(samples) はすべてのサンプルで切断の法則 proj(lift(q)) == q をテストします。

pub fn[S, Q : Eq, A] Section::check(Section[S, Q, A], Array[Q]) -> Bool

Section::check_ops

s.check_ops(quotient, cover, samples) は、samples から作るすべての組について、各演算で proj(op_A(xs.map(lift))) == op_Q(xs) をテストします。

pub fn[S, Q : Eq, A] Section::check_ops(Section[S, Q, A], Algebra[S, Q], Algebra[S, A], Array[Q]) -> Bool

これは代表元上の準同型として proj を確かめます。二つの辞書の演算の並びが一致しないと中断します。

test "section checks" {
  let s : Section[RingSig, Int, BigInt] = Section::of_integral().to_ring()
  assert_true(s.check(ints))
  assert_true(s.check_ops(Algebra::ring(), Algebra::ring(), ints))
}

lift_to(x) は整数値を持ち上げ、証明書なしで任意の FromInteger 対象へ写します。core API に記載しています。

縮約の証人

Reduct

Reduct[S, T] は、すべての S-構造が T-構造でもあり、したがって S-準同型が T-準同型でもあることの証拠です。

pub struct Reduct[S, T] {
  // private fields
}

Reduct はこのパッケージだけが構築できます。

semiring_to_add_monoid, semiring_to_mul_monoid, ring_to_semiring, ring_to_add_group, add_group_to_add_monoid

これらの定数は組み込みシグネチャ間の包含です。

pub let semiring_to_add_monoid : Reduct[SemiringSig, AddMonoidSig]
pub let semiring_to_mul_monoid : Reduct[SemiringSig, MulMonoidSig]
pub let ring_to_semiring : Reduct[RingSig, SemiringSig]
pub let ring_to_add_group : Reduct[RingSig, AddGroupSig]
pub let add_group_to_add_monoid : Reduct[AddGroupSig, AddMonoidSig]

Reduct::refl, Reduct::then

Reduct::refl() は S から自身への自明な包含、r.then(r2) は包含の合成です。

pub fn[S] Reduct::refl() -> Reduct[S, S]
pub fn[S, T, U] Reduct::then(Reduct[S, T], Reduct[T, U]) -> Reduct[S, U]
test "reducts" {
  let r : Reduct[RingSig, AddMonoidSig] = ring_to_add_group.then(add_group_to_add_monoid)
  let h = int64_to_int().forget(r)
  assert_true(h.check(Algebra::add_monoid(), Algebra::add_monoid(), longs))
}

法則の検査

Hom::check

h.check(src, dst, samples) は S のすべての演算について、厳密な等式で準同型の法則をテストします。

pub fn[S, A, B : Eq] Hom::check(Hom[S, A, B], Algebra[S, A], Algebra[S, B], Array[A]) -> Bool

B : Eq が必要です。== を使った check_by です。

Hom::check_by

h.check_by(src, dst, samples, rel) は、samples から作るすべての組について、各演算で rel(f(op_A(xs)), op_B(f(xs))) をテストします。

pub fn[S, A, B] Hom::check_by(Hom[S, A, B], Algebra[S, A], Algebra[S, B], Array[A], (B, B) -> Bool) -> Bool

rel が保存の強さを決めます。厳密な準同型には等式、劣加法的な写像のような緩い準同型には <=、浮動小数点の対象への近似準同型には許容誤差を使います。項数 n の演算は samples.length()^n 個の組でテストされます。src と dst の演算の並びが一致しないと中断します。

test "check_by" {
  let abs : Hom[AddMonoidSig, Double, Double] = Hom::postulate(x => x.abs())
  let samples = [0.0, 1.5, -2.0, 3.25]
  // |x + y| <= |x| + |y|: subadditive, a lax homomorphism
  assert_true(abs.check_by(Algebra::add_monoid(), Algebra::add_monoid(), samples, (l, r) => l <= r))
  assert_false(abs.check(Algebra::add_monoid(), Algebra::add_monoid(), samples))
}

意味論メモ

  • 固定幅の整数ソース（Int、Int64、UInt など）は整数ではなく ℤ/2^k です。そこから BigInt への半環準同型は存在しないため、ℤ への持ち上げは準同型ではなく切断です。同じ議論により Int -> Int64 のような拡幅は準同型ではなく、Int64 -> Int のような切り詰めは環準同型です。
  • 推論規則は証明書を厳密な準同型として合成します。lax（<=）や許容誤差付きの法則しか満たさない写像は、合成後に改めて検査する必要があります。
  • Float と Double を対象とする場合、法則は丸め誤差の範囲でのみ成り立つため、許容誤差付きの check_by を使ってください。core API の埋め込みの説明も参照してください。

非推奨

Hom::from_nat

Hom::from_nat() は NatHomomorphism::from_nat を証明書にします。

#deprecated
pub fn[N : Nat, R : NatHomomorphism] Hom::from_nat() -> Hom[SemiringSig, N, R]

固定幅のソースでは準同型ではありません。代替: Hom::from_integer と Section::of_integral を組み合わせるか、証明書が不要なら lift_to を使います。

Hom::from_integral

Hom::from_integral() は IntegralHomomorphism::from_integral を証明書にします。

#deprecated
pub fn[Z : Integral, R : IntegralHomomorphism] Hom::from_integral() -> Hom[SemiringSig, Z, R]

同じ理由で非推奨で、代替も同じです。