Итак, я читаю немного о разработке, в частности, алгоритмах, основанных на двухцветном исчислении конструкции, и я немного запутался. Я не понимаю, какова цель . Кажется, он идентичен за исключением того, что существует различие между неявными и явными аргументами для функций. В частности, я не...
В « Интуиционистской теории типов: предиктивная часть» Мартина-Лёфа доказано, что проверка типов:a:Aa \colon Aразрешимо при условииaaaбудучи в первую очередь типизируемым , доказывая теорему нормализации для замкнутых типизируемых членов. С другой стороны, я видел, что во многих местах (Википедия,...
Я пытаюсь узнать больше о проверке типов в целых программах и системах вывода типов, которые используют информацию с сайтов вызова функций для вычисления информации о типах (в дополнение к стандартному подходу использования тела функции). Например, такой алгоритм может использовать вызов функции,...
Теорема Кантора утверждает, что Для любого множества A множество всех подмножеств A имеет строго большую мощность, чем само A. Можно ли кодировать что-то подобное, используя только типы / предложения, не обращаясь к наборам ZFC? Код или псевдокод для кодирования этого предложения на зависимо...
Мне было интересно, может ли порядок объявлений индуктивного типа иметь значение. Например, в Coq вы можете определить Natлибо: Inductive Nat := | O : Nat | S : Nat -> Nat. или Inductive Nat := | S : Nat -> Nat | O : Nat. Возможно, это изменит порядок параметров в автоматически...
Функторы, построенные из конечных произведений и сумм, имеют порядковый номер замыкания ωω\omegaподробно описанный в этой рукописи Франсуа Метайера. т.е. мы можем достичь индуктивного типаnat:=μX.1+XNaTзнак равноμИкс,1+Иксnat := \mu X. 1 + X перебирая функтор 1 + Х1+Икс1 + X, которая достигает...
Элементарная аффинная логика - это система типов, которая охватывает класс λ-членов, которые могут быть сокращены за элементарное время Более того, термы типа EAL могут быть сокращены с использованием абстрактного фрагмента алгоритма Лэмпинга, который мне особенно интересен, поскольку я изучаю...
Предположим, что нам не известен результат Джо Б. Уэллса от 1994 года о том, что в System F (AKA неразрешимы и типизация, и проверка типов) λ2λ2\lambda 2). В лямбда-исчислении Барендрегта с типами (1992) я нашел доказательство Малецки 1989 года, что проверка типов подразумевает типизацию. Это...
Меня интересуют проверенные компиляторы, формализованные в теории типов Мартина-Лёфа, т.е. Coq / Agda. На данный момент я написал небольшой игрушечный пример. Тем самым я могу доказать, что мои оптимизации верны. Например, могут быть исключены дополнения с нуля, например, выражения типа «x + 0»....
Большинство зависимых типизированных систем имеют строгие условия положительности для индуктивных типов. Кто-нибудь знает пример, когда нарушение условия приводит к несогласованности в...
Рейнольдс первоначально предложил реляционную семантику для полиморфного лямбда-исчисления второго порядка [1]. Однако позднее он показал [2], что этот подход не согласуется с классической теорией множеств. Питтс описал структуру гипердоктринных моделей и топос-моделей [3], которые согласуются с...