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

групп:

каналов:

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

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

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

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

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

go.backupland.com

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

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

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

Size: a a a

Compiler Development

1014 membersпожаловаться на группу
2021 May 08

B

Brenoritvrezorkre in Compiler Development
Это будут правила вывода самой теории пи-исчисления, просто аксиомы пи-исчисления неплохо перевести в правила вывода, чтобы мы могли с большим удобством манипулировать абстрактными символами пи-исчисления. Да, это будут дополнительные правила вывода к правилам вывода самого лямбда-исчисления, но они должны быть построены в лямбда-определимой форме.
источник
21:46пожаловаться#1

K

Kir in Compiler Development
Мы про вывод типов или что? Так-то есть системы типов, которые вполне тянуть протипировать Y
источник
21:46пожаловаться#2

МБ

Михаил Бахтерев... in Compiler Development
Ну. И Пи-исчисление оно не про полноту. Можно взять CSP, которое не полное, и поведения процессов, всё равно, не выйдет описать только в терминах lambda-исчисления.
источник
21:46пожаловаться#3

B

Brenoritvrezorkre in Compiler Development
Этот комбинатор в нетипизированном лямбда-исчислении приводит к парадоксу Карри.
источник
21:50пожаловаться#4

МБ

Михаил Бахтерев... in Compiler Development
Можно и main сделать. Ну, да, наверное, не на всех ARM. Но некоторые включаются в состоянии, когда указатели стека проинициированы под такой сценарий.
источник
21:51пожаловаться#5

KR

K R in Compiler Development
Нельзя. В С статические переменные должны быть инициализированы до main.
источник
21:54пожаловаться#6

МБ

Михаил Бахтерев... in Compiler Development
У встроенных функций тоже должна быть какая-то семантика. А межпроцессные взаимодействия, кстати, с ленивыми вычислениями не дружат. Для того, чтобы подружить, и нужны монады и seq.

В общим, компиляторщикам хорошо бы знать не только о лямбде.
источник
21:54пожаловаться#7

B

Brenoritvrezorkre in Compiler Development
Как только ты опишешь аксиоматику CSP как правила вывода, и эти правила вывода будут выраженными в терминах лямбда-определимых функций, так сразу ты погружаешь CSP в лямбда-исчисление.
источник
21:54пожаловаться#8

МБ

Михаил Бахтерев... in Compiler Development
Они просто в образ прописываются.
источник
21:54пожаловаться#9

IJ

Igor 🐱 Jirkov in Compiler Development
а чем unsound языки программирования не годятся для программирования?
источник
21:55пожаловаться#10

МБ

Михаил Бахтерев... in Compiler Development
Так вот я и прошу показать, как эти правила вывода выразить лямбда-определимыми функциями.
источник
21:55пожаловаться#11

KR

K R in Compiler Development
Нельзя - они могут быть машинозависимый.
источник
21:57пожаловаться#12

МБ

Михаил Бахтерев... in Compiler Development
Эмс... Так, вроде как, программы на Си компилируются всегда под конкретную машину. Или я опять чего-то не понимаю?
источник
21:58пожаловаться#13

KR

K R in Compiler Development
Вы планку ОЗУ добавили и всё.
источник
21:59пожаловаться#14

B

Brenoritvrezorkre in Compiler Development
Это не про unsoundness. Это парадокс. Он в определённом виде аналогичен парадоксу Рассела, который является парадоксом теории множеств, и семантическим парадоксам (например, лжеца), но при этом он опаснее в том смысле, что не пользуется негацией. В Карри-парадоксальных системах можно доказать что угодно.
источник
22:01пожаловаться#15

МБ

Михаил Бахтерев... in Compiler Development
И что с того? Программа же не знает об этой планке. Как бы, этим занимается OS. Не, ну, можно, конечно писать всё вручную, но тогда и в программе статические переменные будут расположены в разделе, который отображён будет на гарантированно существующую память.
источник
22:01пожаловаться#16

B

Brenoritvrezorkre in Compiler Development
Ну ладно. Потом, как буду в городе, но это очень странный вопрос. Так же, как любые аксиомы, которые переводятся в правила вывода.
источник
22:02пожаловаться#17

МБ

Михаил Бахтерев... in Compiler Development
Ну, способ перевода аксиом в правила вывода я понимаю. А способ перевода правил в функции не очень. Если дадите ссылку, попробую сам разобраться.
источник
22:07пожаловаться#18

IJ

Igor 🐱 Jirkov in Compiler Development
я понимаю это, но как это мешает программировать? Я не говорю сейчас про доказательство теорем в исчислениях вроде CIC, а про условный сермяжный бэкенд
источник
22:08пожаловаться#19

МБ

Михаил Бахтерев... in Compiler Development
Ну, точнее так. Если правила вывода syntax driven, я понимаю, как это делается. А если нет - не представляю. Было бы интересно узнать общий метод.
источник
22:09пожаловаться#20