Опубликованный пакет / CLIR
stacks.sets
v0.1.0Set Theory
Пакет можно напечатать самостоятельным модулем на языке общего назначения, который отвечает без движка правил: ответ и статус, без доказательства, хэшей и канонического документа. Всё на этой странице взято из плана кодогенерации, построенного вместе с индексом; витрина ничего не вычисляет сама.
План кодогенерации
План строится: пакет печатается модулем.
- формат плана
- law-backend-plan/0.7
- возможности
- только базовый слой
Сверка сценариями пакета
Не сверено: сценарии пакета на порождённых модулях не исполнялись. Построенный план ещё не показывает, что ответы совпадают.
Целевые языки
bslcsdarterlexgojavaktluaphppyrbrsscalaswiftts
./law dev backend corpus/clir/stacks-sets.lawir.json --target ts --target py --target go --out DIR
Интерфейс модуля
Вопросы — публичные отношения с производящим правилом; входы — факты, которые вопрос читает. Имена функций следуют языку: ask_… в Python, ask.… в TypeScript, Ask… в Go.
Вопросы · 5
| Имя | Параметры | Смысл | Читает | Источники |
|---|---|---|---|---|
| countable | text | 000D: множество счётно | at_most_aleph_nullcardinality_of | tag/000D |
| exists_ordinal_of_large_cofinality | text | 05N3: существует ординал, кофинальность которого больше данного кардинала, — кофинальность ординала есть наименьшая мощность его конфинального подмножества (000E) | infinite | tag/05N3tag/000E |
| lies_in_some_stage | text | 000C: множество является элементом \(V_α\) для некоторого ординала \(α\) | element_ofhas_rankis_ordinalis_partial_universeis_setstage_of | tag/000Ctag/000B |
| product_is | text, text, text | 000D: произведение первых двух кардиналов равно третьему: \(κ ⊗ λ = μ\) — мощность произведения | at_leastinfinite | tag/000D |
| sum_is | text, text, text | 000D: сумма первых двух кардиналов равна третьему: \(κ ⊕ λ = μ\) — мощность дизъюнктного объединения | at_leastinfinite | tag/000D |
Входы · 10
| Имя | Параметры | Смысл |
|---|---|---|
| at_least | text, text | 000D: первый кардинал не меньше второго в порядке ординалов: \(κ ≥ λ\) |
| at_most_aleph_null | text | 000D: кардинал не превосходит \(ℵ₀\) |
| cardinality_of | text, text | 000D: мощность множества равна кардиналу — наименьшему ординалу, между которым и множеством есть биекция: \(κ = |s|\) |
| element_of | text, text | 000B: множество является элементом частичного универсума: \(s ∈ V_α\) |
| has_rank | text, text | 000B: ранг множества равен ординалу — наименьшему \(α\), для которого \(s ∈ V_{α+1}\) |
| infinite | text | 000D: кардинал бесконечен — он не меньше первого бесконечного кардинала \(ℵ₀ = ω\) |
| is_ordinal | text | 05N1: множество — ординал: транзитивно и вполне упорядочено отношением \(∈\) |
| is_partial_universe | text | 000B: множество — частичный универсум: достаточно большое множество вида \(V_α\), транзитивное по построению |
| is_set | text | 0009: объект есть множество — всякий математический объект разворачивается в множество |
| stage_of | text, text | 000B: частичный универсум есть стадия данного ординала: \(v = V_α\), заданная трансфинитной рекурсией \(V_0 = ∅\), \(V_{α+1} = P(V_α)\), а на предельном \(α\) — объединением предыдущих |