Mar. 30th, 2016

akuklev: (ДР Цертуса 2011)
Напомню, что в теории порядков идеалом называется такое подмножество I предпорядка (O, ≤), что
(а) для любых a b : I найдётся с : I, такой что с ≤ a и с ≤ b,
(b) для любого x : I всякий y ≤ x тоже в I.

Про теорию типов O с сабтайпингом ≤ говорят, что она снабжена иерархией кумулятивных a la Russel вселенных, если задано семейство типов U_i : O, такое, что для каждого T : O найдётся такой U_i, что T : U_i, и семейство U_i образует идеал.

Теории множеств, такие как NBG, оперируют двумя типами сущностей — собственно множествами и классами, среди которых есть proper classes, и классы, представимые множествами. Как известно, если рассмотреть топос, порождённый теорией множеств, то классы играют роль идеалов этого топоса. Представимые множествами классы — это главные идеалы (т.е. порождённые одним элементом), а вот остальные идеалы — proper classes.

Как бы понять, в каком смысле класс Set аналогом идеала расселовских вселенных?..

Как бы понять полиморфную по вселенным квантификацию (∀x : Type) T как class bound quantification, т.е. не как псевдокод, и не как не морфизм из конкретной вселенной U куда-то ещё, а морфизм на уровне идеалов, и как-то увязать это с параметрическим полиморфизмом, как-то увидеть, что если мы не для конкретного типа T, а для всего класса Type имеем id : (∀x : Type) X -> X или NNO : (∀x : Type) (base : X, step : X -> X) -> X, то эти штуки пропозиционально равны функции id и типу Nat соответственно. А в идеале позволить и для главных идеалов порождённых типом X осуществлять номинальную квантификацию (∀x : X) Y, являющуюся ослабленной формой обычного пи-типа (x : T) -> Y, да придать этому смысл в линейных теориях зависимых типов...

December 2016

S M T W T F S
    123
456789 10
11121314151617
18192021222324
25262728293031

Style Credit

Expand Cut Tags

No cut tags
Page generated Sep. 19th, 2017 06:55 pm
Powered by Dreamwidth Studios