В рейтинге участвует:

групп:

каналов:

Виртуальный сервер на SSD - недорого!

Аренда выделенных и виртуальных серверов (VDS/VPS), хостинг, аренда IP-адресов, администрирование, круглосуточная поддержка

qwarta.ru подробнее

Резервное копирование с проверкой на вирусы!!!

Удобный сервис создания резервных копий на любой сервер сети интернет. Отслеживайте изменения, проверяйте на вирусы. Надежно защитите свой бизнес!

go.backupland.com

Выбираете сервер? Любая конфигурация на заказ!

Аренда физических серверов любых конфигураций под любые запросы - 1С бухгалтерия, игровые сервера, нагруженные проекты, интернет-магазины!

qwarta.ru подробнее

Size: a a a

Compiler Development

815 membersпожаловаться на группу
2020 April 17

МБ

Михаил Бахтерев in Compiler Development
Alexander Tchitchigin
По сути, лямбда-терм кодирует дерево вывода...
Ага. Это я понимаю. Не понятно, почему сечение соответствует состоянию, и как стек (вроде как часть состояния) превращается в котерм, то есть, в некоего потребителя значений. Что соответствует этому потреблению?

Речь идёт о call-with-current-continuation?
источник
12:31пожаловаться#1

AG

Alex Gryzlov in Compiler Development
нет, call/cc это производный терм в системе, где есть отрицание
источник
12:39пожаловаться#2

AG

Alex Gryzlov in Compiler Development
лямбда-мю или ее секвент-аналоги
источник
12:39пожаловаться#3

AG

Alex Gryzlov in Compiler Development
callcc : Term g ((a~>b)~>a) (a::d) -> Term g a d
callcc f = Mu $ Named Here $ App f (Lam $ Mu $ Named (There Here) (Var Here))
источник
12:41пожаловаться#4

AG

Alex Gryzlov in Compiler Development
или, если в логической форме

pierce : Term g (((a~>b)~>a)~>a) d
pierce = Lam $ Mu $ Named Here $ App (Var Here) (Lam $ Mu $ Named (There Here) (Var Here))
источник
12:42пожаловаться#5

AG

Alex Gryzlov in Compiler Development
стек это ведь такая же структура данных, и нам ничего не мешает его вшить в исчисление
источник
12:44пожаловаться#6

ЗП

Зигохистоморфный Препроморфизм in Compiler Development
Alex Gryzlov
или, если в логической форме

pierce : Term g (((a~>b)~>a)~>a) d
pierce = Lam $ Mu $ Named Here $ App (Var Here) (Lam $ Mu $ Named (There Here) (Var Here))
lambda-mu с адресацией перехода?
источник
12:44пожаловаться#7

AG

Alex Gryzlov in Compiler Development
да, с covariables
источник
12:44пожаловаться#8

ЗП

Зигохистоморфный Препроморфизм in Compiler Development
этот тот хак, что позволяет выражать классическую логику и ее законы
источник
12:45пожаловаться#9

AG

Alex Gryzlov in Compiler Development
это не хак, просто такая вычислительная интерпретация, через продолжения
источник
12:45пожаловаться#10

ИЧ

Илья Чистяков in Compiler Development
что почитать на русском чтоб понять текущий топик? только не лекции по категориям..
источник
12:45пожаловаться#11

AG

Alex Gryzlov in Compiler Development
категории здесь не особо помогут, хотя конечно есть такая штука как категорная логика
источник
12:46пожаловаться#12

ЗП

Зигохистоморфный Препроморфизм in Compiler Development
Alex Gryzlov
это не хак, просто такая вычислительная интерпретация, через продолжения
ну моментальная замена всего терма по адресу
источник
12:46пожаловаться#13

ИЧ

Илья Чистяков in Compiler Development
Alex Gryzlov
категории здесь не особо помогут, хотя конечно есть такая штука как категорная логика
в категориях есть ко-что-то-там как, вот и подумал
источник
12:47пожаловаться#14

AG

Alex Gryzlov in Compiler Development
да, вот Михаила тоже эта терминология смутила
источник
12:47пожаловаться#15

AG

Alex Gryzlov in Compiler Development
на русском даже не знаю, поищите учебник по теории доказательств наверно
источник
12:48пожаловаться#16

ИЧ

Илья Чистяков in Compiler Development
пасиб, попробую
источник
12:48пожаловаться#17

AT

Alexander Tchitchigin in Compiler Development
Если начинать прямо с мат. логики, что часто классический учебник Клини советуют. Не помню, насколько он там углубляется в секвенции и естественный вывод, правда.
источник
12:49пожаловаться#18

ИЧ

Илья Чистяков in Compiler Development
спасибо
источник
12:56пожаловаться#19

ЗП

Зигохистоморфный Препроморфизм in Compiler Development
@clayrat удивительно, чего lambda-mu нет в https://wiki2.org/en/Lambda_cube
wiki2.org
Lambda cube - Wikipedia Republished // WIKI 2
In mathematical logic and type theory, the λ-cube is a framework introduced by Henk Barendregt  to investigate the different dimensions in which the calculus of constructions is a generalization of the simply typed λ-calculus. Each dimension of the cube corresponds to a new kind of dependency between terms and types. Here, "dependency" refers to the capacity of a term or type to bind a term or type. The respective dimensions of the λ-cube correspond to:
источник
13:25пожаловаться#20