core API

Luna-Flow/luna-poly/core はライブラリ全体で共有される語彙を定めるパッケージです。指数ベクトルによる単項式型、名前付き変数の層、形状メタデータ、すべての具体的な多項式が実装する能力トレイト、そして辞書渡し方式のジェネリックコードで使う演算レコードを提供します。多項式の格納形式そのものは持ちません。

2 つのファサード immut と mutable はこのページのすべての型とトレイトを再エクスポートするため、ほとんどのプログラムは core を直接インポートする必要がありません。直接インポートする場合は、Luna-Flow/type_theory/core と衝突しない別名を付けてください:

import {
  "Luna-Flow/luna-poly/core" @poly_core,
}

このページの例ではその別名を使います。各項目の背後にある数学は core の設計で説明しています。

単項式

`ExponentVector`

ExponentVector は単項式 $x^\alpha = x_0^{\alpha_0} x_1^{\alpha_1} \cdots$ の指数ベクトル $\alpha = (\alpha_0, \alpha_1, \dots)$ です。末尾のゼロ指数は格納されないため、[1, 0] と [1] は同じ値であり、全次数 $|\alpha| = \sum_i \alpha_i$ はキャッシュされます。

type ExponentVector derive(@debug.Debug)
pub impl @luna-generic.One for ExponentVector
pub impl Compare for ExponentVector
pub impl Eq for ExponentVector
pub impl Hash for ExponentVector
pub impl Mul for ExponentVector
pub impl Show for ExponentVector

値はイミュータブルです。「更新」はすべて新しいベクトルを返します。

`ExponentVector::from_array`

配列から末尾のゼロを取り除き、正規形の指数ベクトルを構築します。配列はコピーされます。

pub fn ExponentVector::from_array(Array[UInt]) -> Self

`ExponentVector::one`

空の指数ベクトル、すなわち単項式 $1 = x^{0}$ を返します。これは ExponentVector に対する One::one() でもあります。

pub fn ExponentVector::one() -> Self

`ExponentVector::length`

格納されている長さを返します。これは最後の非ゼロ指数のインデックスに 1 を加えた値で、単位元では 0 です。

pub fn ExponentVector::length(Self) -> Int

`ExponentVector::degree`

全次数 $|\alpha| = \sum_i \alpha_i$ を $O(1)$ で返します。

pub fn ExponentVector::degree(Self) -> UInt

次数は UInt の和なので、指数がそれほど大きい場合は $2^{32}$ を法としてラップアラウンドします。

`ExponentVector::is_one`

単位ベクトル(すべての指数がゼロ)の場合に限り true を返します。

pub fn ExponentVector::is_one(Self) -> Bool

`ExponentVector::get`

変数 index の指数を返します。v[index] としても使えます。length() 以上のインデックスは 0 として読まれます。負のインデックスでは中断 (abort) します。

#alias("_[_]")
pub fn ExponentVector::get(Self, Int) -> UInt

`ExponentVector::get_checked`

get と同様に Some(exponent) を返しますが、負のインデックスでは None を返します。

pub fn ExponentVector::get_checked(Self, Int) -> UInt?

`ExponentVector::with_exponent`

index の指数を value に置き換え、再び正規化した新しいベクトルを返します(最後の非ゼロ指数を 0 にするとベクトルは短くなります)。負のインデックスでは中断 (abort) します。

pub fn ExponentVector::with_exponent(Self, Int, UInt) -> Self

`ExponentVector::with_exponent_checked`

負のインデックスでは None を返し、それ以外では with_exponent の結果を Some に包んで返します。

pub fn ExponentVector::with_exponent_checked(Self, Int, UInt) -> Self?

`ExponentVector::to_array`

末尾のゼロを含まない正規形の指数を新しくコピーして返します。

pub fn ExponentVector::to_array(Self) -> Array[UInt]

`ExponentVector::mul`

指数を成分ごとに加えて 2 つの単項式を掛けます: $x^\alpha x^\beta = x^{\alpha+\beta}$ 。これは * 演算子でもあります。

pub fn ExponentVector::mul(Self, Self) -> Self

指数の加算は UInt の加算であり、 $2^{32}$ を法としてラップアラウンドします。

`ExponentVector::compare`

ライブラリの単項式順序で 2 つの単項式を比較します。まず全次数で比較し、次に両者が異なる変数のうち最もインデックスの大きい変数の指数で比較して、指数が大きい方を大きい単項式とします。これは $x_0 < x_1 < x_2 < \cdots$ とした次数付き辞書式順序です。<、<=、>、>= もこの比較に基づきます。

pub fn ExponentVector::compare(Self, Self) -> Int

この順序は全順序であり、 $1$ を最小元とし、乗法と両立します: $\alpha < \beta$ ならば $\alpha + \gamma < \beta + \gamma$ です。これらの性質は core の設計で導出しています。

`ExponentVector::equal`, `ExponentVector::hash`

equal は正規形ベクトルの構造的等価性(==)であり、hash はそれと整合します。

pub fn ExponentVector::equal(Self, Self) -> Bool
pub fn ExponentVector::hash(Self) -> Int

`ExponentVector::to_string`

変数 0 を x、変数 i を x_i、単位元を 1 として単項式を文字列化します。因子は区切りなしで並べて書かれます。

pub fn ExponentVector::to_string(Self) -> String

test "exponent vectors" {
  let a = @poly_core.ExponentVector::from_array([2U, 0, 1, 0])
  debug_inspect(a.to_array(), content="[2, 0, 1]")
  inspect(a.degree(), content="3")
  inspect(a[1], content="0")
  inspect(a[7], content="0")
  inspect(a, content="x^2x_2")
  let b = @poly_core.ExponentVector::from_array([0U, 1])
  inspect(a * b, content="x^2x_1x_2")
  assert_true(a.get_checked(-1) is None)
  assert_true(a.with_exponent(2, 0) == @poly_core.ExponentVector::from_array([2U]))
  // Same degree: the higher variable decides, so x_1 > x_0.
  let x0 = @poly_core.ExponentVector::from_array([1U])
  let x1 = @poly_core.ExponentVector::from_array([0U, 1])
  assert_true(x0 < x1)
  assert_true(x1 < x0 * x0)
}

名前付き変数

`Variable`

Variable は名前付き変数と、それを作成した VariableContext 内での位置との組です。2 つの変数は名前とインデックスの両方が一致するとき等しくなります。

type Variable derive(Compare, Eq, @debug.Debug)
pub impl Show for Variable

変数はコンテキストから取得します。公開コンストラクタはありません。

`Variable::name`, `Variable::index`

name は変数の名前を返し、index はコンテキスト内での位置を返します。この位置は ExponentVector における指数の位置でもあります。

pub fn Variable::name(Self) -> String
pub fn Variable::index(Self) -> Int

`Variable::to_type_theory_name`

変数の名前を Luna-Flow/type_theory の Name として返します。インデックスは結果に含まれません。インデックスは VariableContext::variable_by_type_theory_name でコンテキスト内の名前を検索して復元します。

pub fn Variable::to_type_theory_name(Self) -> @Luna-Flow/type_theory/core.Name

`Variable::compare`, `Variable::equal`, `Variable::to_string`

compare は変数を名前、次にインデックスの順で比較し(導出実装)、equal は名前とインデックスを比較し、to_string は名前を返します。

pub fn Variable::compare(Self, Self) -> Int
pub fn Variable::equal(Self, Self) -> Bool
pub fn Variable::to_string(Self) -> String

`VariableContext`

VariableContext は互いに異なる変数名からなる、順序付きの永続的な表です。位置 $i$ の変数はインデックス $i$ を持ち、名前は一意なので、1 つのコンテキスト内では名前とインデックスが互いを決定します。

type VariableContext derive(Eq, @debug.Debug)
pub impl Show for VariableContext

コンテキストは構造的に比較されます。同じ名前を同じ順序で持つ 2 つのコンテキストは、どこで構築されたかに関係なく等しくなります。

`VariableContext::new`

空のコンテキストを返します。

pub fn VariableContext::new() -> Self

`VariableContext::from_names`

names を順に変数とするコンテキストを構築します。名前が重複すると中断 (abort) します。

pub fn VariableContext::from_names(Array[String]) -> Self

`VariableContext::from_names_checked`

from_names と同様ですが、名前が 2 回現れた場合は None を返します。

pub fn VariableContext::from_names_checked(Array[String]) -> Self?

`VariableContext::extend_checked`

name を末尾に追加した新しいコンテキストと新しい変数の組を返します。名前がすでに存在する場合は None を返します。レシーバは変更されません。

pub fn VariableContext::extend_checked(Self, String) -> (Self, Variable)?

`VariableContext::extend_with`

extend_checked と同様ですが、名前が重複すると中断 (abort) します。

#alias(extend, deprecated)
pub fn VariableContext::extend_with(Self, String) -> (Self, Variable)

旧名 extend は非推奨の別名として残されています。非推奨を参照してください。

`VariableContext::size`, `VariableContext::variables`, `VariableContext::get`

size は変数の個数を返し、variables は変数をインデックス順に並べた新しい配列を返し、get はインデックス位置の変数を返します。0 ..< size() の範囲外では None を返します。

pub fn VariableContext::size(Self) -> Int
pub fn VariableContext::variables(Self) -> Array[Variable]
pub fn VariableContext::get(Self, Int) -> Variable?

`VariableContext::variable`, `VariableContext::require_variable`

variable は名前で変数を検索し、存在しなければ None を返します。require_variable は代わりに中断 (abort) します。検索は線形走査です。

pub fn VariableContext::variable(Self, String) -> Variable?
pub fn VariableContext::require_variable(Self, String) -> Variable

`VariableContext::contains`

コンテキストの variable.index() 位置にある変数が variable と等しいとき true を返します。したがって、構造的に等しいコンテキストの変数も含まれているとみなされます。

pub fn VariableContext::contains(Self, Variable) -> Bool

`VariableContext::variable_by_type_theory_name`

type_theory の Name を、同じテキストを持つ変数に解決します。見つからなければ None を返します。

pub fn VariableContext::variable_by_type_theory_name(Self, @Luna-Flow/type_theory/core.Name) -> Variable?

コンテキスト c のすべての変数 v について、c.variable_by_type_theory_name(v.to_type_theory_name()) == Some(v) が成り立ちます。

`VariableContext::require_type_theory_name`

variable_by_type_theory_name と同様ですが、名前が未知の場合は中断 (abort) します。

pub fn VariableContext::require_type_theory_name(Self, @Luna-Flow/type_theory/core.Name) -> Variable

`VariableContext::equal`

構造的等価性です。== としても使えます。

pub fn VariableContext::equal(Self, Self) -> Bool

test "variable contexts" {
  let ctx = @poly_core.VariableContext::from_names(["x", "y"])
  inspect(ctx, content="VariableContext(x, y)")
  let (ctx2, z) = ctx.extend_with("z")
  inspect(z.index(), content="2")
  inspect(ctx.size(), content="2")
  assert_true(ctx.extend_checked("x") is None)
  assert_true(@poly_core.VariableContext::from_names_checked(["a", "a"]) is None)
  let y = ctx2.require_variable("y")
  let name = y.to_type_theory_name()
  inspect(name.text(), content="y")
  assert_true(ctx2.variable_by_type_theory_name(name) == Some(y))
  assert_true(ctx2.variable_by_type_theory_name(@tt_core.Name::new("w")) is None)
  assert_true(ctx.contains(y))
  assert_false(ctx.contains(z))
}

形状

`PolynomialShape`

PolynomialShape は多項式の係数を除いた寸法を表します。以下のスネークケースの関数またはコンストラクタで構築します。

pub enum PolynomialShape {
  Univariate(length~ : Int)
  Multivariate(arity~ : Int, term_count~ : Int)
  Contextual(context~ : VariableContext, arity~ : Int, term_count~ : Int)
} derive(Eq, @debug.Debug)
pub fn PolynomialShape::equal(Self, Self) -> Bool

length は密多項式に格納された係数の個数、arity は使用されている変数の個数(最も長い指数ベクトルの長さ)、term_count は非ゼロ項の個数です。

`PolynomialShape::univariate`, `PolynomialShape::multivariate`, `PolynomialShape::contextual`

3 種類の形状を構築します。

pub fn PolynomialShape::univariate(Int) -> Self
pub fn PolynomialShape::multivariate(Int, Int) -> Self
pub fn PolynomialShape::contextual(VariableContext, Int, Int) -> Self

`PolynomialShape::arity`

アリティを返します。一変数の形状のアリティは 1 です。

pub fn PolynomialShape::arity(Self) -> Int

`PolynomialShape::term_count`

項数を返します。一変数の形状は項数を記録しないため None を返します。

pub fn PolynomialShape::term_count(Self) -> Int?

`PolynomialShape::is_compatible_with`

2 つの形状の値を組み合わせられるとき true を返します。すなわち、2 つの一変数形状、2 つの多変数形状、または等しいコンテキスト上の 2 つのコンテキスト付き形状の場合です。アリティと項数は無視されます。

pub fn PolynomialShape::is_compatible_with(Self, Self) -> Bool

`PolynomialShape::compatible_checked`

Option のパイプラインで使えるよう、形状が両立するとき Some(()) を、そうでないとき None を返します。

pub fn PolynomialShape::compatible_checked(Self, Self) -> Unit?

test "shapes" {
  let ctx = @poly_core.VariableContext::from_names(["x"])
  let a = @poly_core.PolynomialShape::multivariate(2, 5)
  let b = @poly_core.PolynomialShape::multivariate(3, 1)
  let c = @poly_core.PolynomialShape::contextual(ctx, 1, 1)
  assert_true(a.is_compatible_with(b))
  assert_false(a.is_compatible_with(c))
  inspect(a.arity(), content="2")
  assert_true(@poly_core.PolynomialShape::univariate(4).term_count() is None)
  assert_true(c.compatible_checked(c) is Some(_))
}

能力トレイト

能力トレイトは、それぞれ 1 つの観測可能な性質を表す小さな開いたトレイト (pub(open)) です。バンドルトレイトはそれらを、ジェネリックコードが通常必要とする形にまとめます。ライブラリのすべての具体的な多項式型は、次の表に挙げるバンドルを実装しています:

トレイト	必須メソッド / スーパートレイト	実装する型
`UnivariatePolynomial`	`HasShape + HasLength + HasDegree + IsZero`	`DensePolynomial`
`MultivariatePolynomial`	`HasShape + HasTermCount + HasArity + HasTotalDegree + IsZero`	`TermPolynomial`, `SparsePolynomial`
`ContextualPolynomial`	`HasShape + HasContext + HasTermCount + HasArity + IsZero`	`ContextPolynomial`
`MutablePolynomial`	`Clearable + Copyable`	すべての `mutable` コンテナ

`HasLength`

密多項式に格納された係数の個数。ゼロ多項式では 0。

pub(open) trait HasLength {
  fn length(Self) -> Int
}

`HasDegree`

一変数多項式の次数。ゼロ多項式では None。

pub(open) trait HasDegree {
  fn degree(Self) -> Int?
}

`IsZero`

値がゼロ多項式かどうか。正規形では「格納された項がない」ことと同じです。

pub(open) trait IsZero {
  fn is_zero(Self) -> Bool
}

`HasTermCount`

非ゼロ項の個数。

pub(open) trait HasTermCount {
  fn term_count(Self) -> Int
}

`HasArity`

使用されている変数の個数。すべての項にわたる ExponentVector::length の最大値で、定数では 0。

pub(open) trait HasArity {
  fn arity(Self) -> Int
}

`HasTotalDegree`

すべての項にわたる全次数の最大値。ゼロ多項式では None。

pub(open) trait HasTotalDegree {
  fn total_degree(Self) -> UInt?
}

`HasContext`

多項式が束縛されている変数コンテキスト。

pub(open) trait HasContext {
  fn context(Self) -> VariableContext
}

`HasShape`

値の PolynomialShape。

pub(open) trait HasShape {
  fn shape(Self) -> PolynomialShape
}

`Clearable`

ミュータブルなコンテナをその場でゼロにリセットします。

pub(open) trait Clearable {
  fn clear(Self) -> Unit
}

`Copyable`

ミュータブルなコンテナの独立したコピーを返します。以後どちらの値を変更しても、もう一方には影響しません。

pub(open) trait Copyable {
  fn copy(Self) -> Self
}

`UnivariatePolynomial`

密な一変数多項式のためのバンドル。

pub(open) trait UnivariatePolynomial : HasShape + HasLength + HasDegree + IsZero {
}

`MultivariatePolynomial`

インデックスで変数を指定する多変数多項式のためのバンドル。

pub(open) trait MultivariatePolynomial : HasShape + HasTermCount + HasArity + HasTotalDegree + IsZero {
}

`ContextualPolynomial`

VariableContext に束縛された多項式のためのバンドル。

pub(open) trait ContextualPolynomial : HasShape + HasContext + HasTermCount + HasArity + IsZero {
}

`MutablePolynomial`

ミュータブルなコンテナのためのバンドル。

pub(open) trait MutablePolynomial : Clearable + Copyable {
}

fn[P : @poly_core.MultivariatePolynomial] describe(p : P) -> String {
  let degree = match @poly_core.HasTotalDegree::total_degree(p) {
    Some(d) => d.to_string()
    None => "-"
  }
  "terms=\{@poly_core.HasTermCount::term_count(p)} arity=\{@poly_core.HasArity::arity(p)} degree=\{degree}"
}

test "capability traits" {
  let term = @immut.TermPolynomial::from_array([([2U, 1], 3), ([], 1)])
  let sparse = @immut.SparsePolynomial::from_array([([2U, 1], 3), ([], 1)])
  inspect(describe(term), content="terms=2 arity=2 degree=3")
  inspect(describe(sparse), content="terms=2 arity=2 degree=3")
}

複数のトレイト境界を持つ関数の中では、上の例のようにトレイトメソッドを修飾形式 Trait::method(value) で呼び出してください。

演算レコード

MoonBit のトレイトは型パラメータとして Self しか持てないため、「係数型 A を持つ多項式型 P」をトレイトで表現できません。演算レコードはこの隙間を埋めます。各具体型は ops() メソッドから関数のレコードを返し、ジェネリックコードはそのレコードを通常の引数として受け取ります。アクセサメソッドは格納された関数を呼び出すだけで、独自の振る舞いは追加しません。

`UnivariateOps`

係数 A を持つ一変数多項式型 P の演算。

type UnivariateOps[P, A]
pub fn[P, A] UnivariateOps::new(() -> P, () -> P, (Array[A]) -> P, (P) -> Array[A], (P, Int) -> A, (P, Int) -> A?, (P, A) -> A, (P, P) -> P, (P, P) -> P, (P, Int, A) -> P, (P, Int, A) -> P?, (P, UInt) -> P) -> Self[P, A]

new は順に zero、one、from_coefficients、to_coefficients、coefficient、coefficient_checked、eval、add、mul、scale、scale_checked、pow を受け取ります。意味は DensePolynomial の同名メソッドと同じです。独自の一変数多項式型をラップするのに使います。

`UnivariateOps` のアクセサ

各アクセサは対応する格納済みの関数を適用します。

pub fn[P, A] UnivariateOps::zero(Self[P, A]) -> P
pub fn[P, A] UnivariateOps::one(Self[P, A]) -> P
pub fn[P, A] UnivariateOps::from_coefficients(Self[P, A], Array[A]) -> P
pub fn[P, A] UnivariateOps::to_coefficients(Self[P, A], P) -> Array[A]
pub fn[P, A] UnivariateOps::coefficient(Self[P, A], P, Int) -> A
pub fn[P, A] UnivariateOps::coefficient_checked(Self[P, A], P, Int) -> A?
pub fn[P, A] UnivariateOps::eval(Self[P, A], P, A) -> A
pub fn[P, A] UnivariateOps::add(Self[P, A], P, P) -> P
pub fn[P, A] UnivariateOps::mul(Self[P, A], P, P) -> P
pub fn[P, A] UnivariateOps::scale(Self[P, A], P, Int, A) -> P
pub fn[P, A] UnivariateOps::scale_checked(Self[P, A], P, Int, A) -> P?
pub fn[P, A] UnivariateOps::pow(Self[P, A], P, UInt) -> P

`MultivariateOps`

係数 A を持つ、インデックスで変数を指定する多変数多項式型 P の演算。

type MultivariateOps[P, A]
pub fn[P, A] MultivariateOps::new(() -> P, () -> P, (Array[(ExponentVector, A)]) -> P, (P) -> Array[(ExponentVector, A)], (P, Array[A]) -> A, (P, Array[A]) -> A?, (P, P) -> P, (P, P) -> P, (P, ExponentVector, A) -> P, (P, UInt) -> P) -> Self[P, A]

new は順に zero、one、from_terms、to_terms、eval_indexed、eval_indexed_checked、add、mul、scale、pow を受け取ります。eval_indexed は TermPolynomial および SparsePolynomial の eval メソッドに相当します。

`MultivariateOps` のアクセサ

pub fn[P, A] MultivariateOps::zero(Self[P, A]) -> P
pub fn[P, A] MultivariateOps::one(Self[P, A]) -> P
pub fn[P, A] MultivariateOps::from_terms(Self[P, A], Array[(ExponentVector, A)]) -> P
pub fn[P, A] MultivariateOps::to_terms(Self[P, A], P) -> Array[(ExponentVector, A)]
pub fn[P, A] MultivariateOps::eval_indexed(Self[P, A], P, Array[A]) -> A
pub fn[P, A] MultivariateOps::eval_indexed_checked(Self[P, A], P, Array[A]) -> A?
pub fn[P, A] MultivariateOps::add(Self[P, A], P, P) -> P
pub fn[P, A] MultivariateOps::mul(Self[P, A], P, P) -> P
pub fn[P, A] MultivariateOps::scale(Self[P, A], P, ExponentVector, A) -> P
pub fn[P, A] MultivariateOps::pow(Self[P, A], P, UInt) -> P

`ContextOps`

係数 A を持つ、コンテキストに束縛された多項式型 P の演算。

type ContextOps[P, A]
pub fn[P, A] ContextOps::new((VariableContext, Array[(ExponentVector, A)]) -> P, (P) -> Array[(ExponentVector, A)], (P, Array[(Variable, A)]) -> A?, (P, P) -> P?, (P, P) -> P?) -> Self[P, A]

new は順に from_terms、to_terms、eval_named_checked、add_checked、mul_checked を受け取ります。意味は ContextPolynomial の同名メソッドと同じです。

`ContextOps` のアクセサ

pub fn[P, A] ContextOps::from_terms(Self[P, A], VariableContext, Array[(ExponentVector, A)]) -> P
pub fn[P, A] ContextOps::to_terms(Self[P, A], P) -> Array[(ExponentVector, A)]
pub fn[P, A] ContextOps::eval_named_checked(Self[P, A], P, Array[(Variable, A)]) -> A?
pub fn[P, A] ContextOps::add_checked(Self[P, A], P, P) -> P?
pub fn[P, A] ContextOps::mul_checked(Self[P, A], P, P) -> P?

fn[P, A] sum_of_squares(ops : @poly_core.MultivariateOps[P, A], polys : Array[P]) -> P {
  let mut acc = ops.zero()
  for p in polys {
    acc = ops.add(acc, ops.pow(p, 2))
  }
  acc
}

test "operation records" {
  let x = @immut.SparsePolynomial::from_array([([1U], 1)])
  let y = @immut.SparsePolynomial::from_array([([0U, 1], 1)])
  let ops = @immut.SparsePolynomial::ops()
  let s = sum_of_squares(ops, [x, y])
  inspect(s, content="1 * x^2 + 1 * x_1^2")
  inspect(ops.eval_indexed(s, [3, 4]), content="25")
}

非推奨

非推奨	代替
`VariableContext::extend`	`VariableContext::extend_with`(振る舞いは同じ。`extend` は現在予約語です)
`ExponentVector`、`Variable`、`VariableContext`、`PolynomialShape` の `not_equal`、`op_lt`、`op_le`、`op_gt`、`op_ge` メソッド	演算子 `!=`、`<`、`<=`、`>`、`>=`
`output` メソッド(`Show` 由来)	`to_string` または文字列補間
`to_repr` メソッド(`Debug` 由来)	`Repr(x)` または `debug_inspect`
`ExponentVector::hash_combine`	トレイト経由の `Hash::hash_combine`

最後の 4 行のメソッド形式はインターフェースファイルから隠されており、ソース互換性のためだけに残されています。

core API

単項式

ExponentVector

ExponentVector::from_array

ExponentVector::one

ExponentVector::length

ExponentVector::degree

ExponentVector::is_one

ExponentVector::get

ExponentVector::get_checked

ExponentVector::with_exponent

ExponentVector::with_exponent_checked

ExponentVector::to_array

ExponentVector::mul

ExponentVector::compare

ExponentVector::equal, ExponentVector::hash

ExponentVector::to_string

名前付き変数

Variable

Variable::name, Variable::index

Variable::to_type_theory_name

Variable::compare, Variable::equal, Variable::to_string

VariableContext

VariableContext::new

VariableContext::from_names

VariableContext::from_names_checked

VariableContext::extend_checked

VariableContext::extend_with

VariableContext::size, VariableContext::variables, VariableContext::get

VariableContext::variable, VariableContext::require_variable

VariableContext::contains

VariableContext::variable_by_type_theory_name

VariableContext::require_type_theory_name

VariableContext::equal

形状

PolynomialShape

PolynomialShape::univariate, PolynomialShape::multivariate, PolynomialShape::contextual

PolynomialShape::arity

PolynomialShape::term_count

PolynomialShape::is_compatible_with

PolynomialShape::compatible_checked