> categories where the interpretation of the rules of the MLTT is given А этот набор категорий вообще формально определён?
Мне что-то вообще непонятно, зачем пытаться выжать из LLM полностью формальные рассуждения, при этом даже не пытаясь ей объяснить, что именно ты от неё хочешь (контекст)? Звуч...
А если мы конечные наты определим в теории типов при помощи рекурсии-индукции или рекурсии-рекурсии или типа того? Примерно так: 1. 0 — натуральное число 2. suc n — натурально...
https://www.findaphd.com/phds/project/automated-verification-of-webassembly-programs/?p169824 Fully funded PhD scholarship with Graduate Teaching Assistantship in Automated Ve...
Я что-то не понимаю, какая проблема топологически сортернуть конечный граф? 🧐
Собственно, кардинальность множества не является ли (дискретной) мерой? Я не шарю.
Я, кстати, не понял, что именно считается "спекулятивной оптимизацией"? Inline caches считаются? Девиртуализация + inline?
https://www.opennet.ru/opennews/art.shtml?num=59986 Исследователи из Швейцарской высшей технической школы Цюриха разработали систему fuzzing-тестирования Cascade, нацеленную н...
@Yaroslav_Schekin можете, пожалуйста, растолковать где проходит граница между неоднозначной КС грамматикой, для которой мы потом делаем disambiguation на основе информации из ...
Может быть, кому-либо будет интересно: Greetings! This is just a reminder of the following coming online lecture on Logic and foundations of mathematics by Prof. Richard Zach...
Я тут на днях напрограммировал: https://gist.github.com/gabriel-fallen/5b7d5b7131188d53cfeafd439f47b946 Разъесните, пожалуйста, @napa3um какие автоматы и переходы я там описа...
if_then_else_block: KW_If exp then_block else_block? KW_End; then_block: KW_Then? block; @Fancryer Вы уверены в отсутствии неоднозначности с опциональным KW_Then? Особенно учи...
В связи с недавним спором возник вопрос теоретического свойства... Как известно (простите, что повторяю базовые определения), доказательство в системе Гильбертовского типа — ...
https://obua.com/publications/indentation-sensitive-parsing-with-pyramids/1/ Для любителей парсинга и странных грамматик. Что-то про "Local Lexing" — лексический разбор, кото...
С мест сообщают: https://www.opennet.ru/opennews/art.shtml?num=54918
Я тут подумал такую мысль. Языки, которые производят нативный бинарник типа Go/D/Haskell/OCaml, вставляют GC в конкретную программу, т.е. в каждом отдельном случае GC должен х...
Следующее заседание состоится в четверг 16 декабря 2021 г. с 14:00 до 15:30 московского времени (18:00-19:30 в Новосибирске) и пройдет онлайн в Zoom, подключиться к конференци...
В любом случае — а зачем его сохранять?
@qweasdzxcrtyfghvbnuioj https://github.com/lalrpop/lalrpop maybe? I dunno...
https://twitter.com/jckarter/status/1428093469755527168?s=20