SK
в дейли была пара бесполезных статей по поводу
Size: a a a
2020 April 29
SK
и в чечне обсуждение короткое
Oℕ
Но всё-таки что такое фуел паттерн тогда? Доказательство свойств для некоторых бесконечных процессов или вроде того?
Oℕ
всё бы так писали
AG
Но всё-таки что такое фуел паттерн тогда? Доказательство свойств для некоторых бесконечных процессов или вроде того?
это когда не можешь доказать тотальность, и цепляешь дополнительным параметром нат с лимитом шагов
AG
лимит закончился и досвидос
SK
сперли идею с оптимизаций в компиляторах
AG
в эфиреум в свою очередь идею поперли вторично и назвали gas
AG
про логические реляции еще кстати можно добавить что одним из базовых примеров этой техники является пресловутое NbE
SK
(normalization by evaluation)
SK
NBE for simple types uses a logical relation between the syntax and the presheaf interpretation
SK
прикольно, не задумывался
S
DM
начинал, но вышел только из здания