AG
это получается абстрактная машина
Size: a a a
2020 April 17
AG
если вы распишете теперь типы у стека, то получится структура дуальная термам
AG
так вот оказывается что это в точности древнее генценовское исчисление секвенций
AG
вот и все
AG
там нет никаких особых двойных подтекстов, вся теория доказательств по определению чисто синтаксическая, в отличие от теории моделей скажем
AG
наверняка это все красиво натягивается на функторы подстановки и прочий катлог, но это уже следующий уровень
МБ
если вы распишете теперь типы у стека, то получится структура дуальная термам
Это я делал с Машиной Кривина. Но что-то картина не складывается. Пойду ещё раз статью перечитаю. Спасибо за пояснения
AG
я тут веду онлайн семинарчики по этой теме, можете посмотреть видосы и код
2020 April 18
ЗП
есть язык с ядром не с Lambda Calculus, а с Kappa Сalculus?
АЕ
В процессе разработки компилятора языка Оберон, мы составили вот такие схемы, помогающие на примере понять, какую форму принимает символьная таблица в тех или иных случаях. Оберон — императивный, компилируемый в машинный код язык. Видимые на схемах конструкции существуют только во время компиляции.
На схемах рассматриваются следующие аспекты:
1) предопределённые типы,
2) объявление переменной, типа, процедуры,
3) импорт модуля, содержащего процедуру.
С ходом развития проекта и с кодом компилятора можно ознакомиться здесь:
https://github.com/kekcleader/oberon
На схемах рассматриваются следующие аспекты:
1) предопределённые типы,
2) объявление переменной, типа, процедуры,
3) импорт модуля, содержащего процедуру.
С ходом развития проекта и с кодом компилятора можно ознакомиться здесь:
https://github.com/kekcleader/oberon
DP
кто-нибудь видел Handbook of Automated Reasoning Robinson Voronkov ?
KR
Dmitry Ponyatov
кто-нибудь видел Handbook of Automated Reasoning Robinson Voronkov ?
DP
круто, спасибо
r
Ой, вот такого рода "знакомство с Haskell" бы только повредило, на мой взгляд. Ведь все очень просто, автору хорошо бы идти от существа задачи. Есть очень мощный подход: представьте, что уже имеется подходящая нотация для описания решения задачи, далее просто опишите решение. А затем реализуйте и нотацию. В данном случае выразительным описанием, очевидно, выступает грамматика в БНФ. И в дело вступают технические моменты, как грамматику выразить прямо на JS, что для этого нужно. Гораздо хуже, когда человек начинает думать в терминах шаблонов проектирования изначально. В этом смысле неважно, речь ли об ООП, или о ФП.
「 Есть очень мощный подход: представьте, что уже имеется подходящая нотация для описания решения задачи, далее просто опишите решение. А затем реализуйте и нотацию. 」
Да, это действительно очень мощный подход.
Но, мне кажется, разные языки дают разную поддержку для этого подхода. Т.е., в одних языках проще получается реализовывать свои концепции, а в других — сложней. Один язык/компилятор бьет тебя по рукам, или вынуждает городить длинные конструкции, а другой — даже позволяет стрелять себе в ногу ;)
Наверное, это можно назвать мощностью выразительных средств языка. Как по вашему, возможно ли как-то более-менее объективно упорядочить языки по этой величине?
Или тут больше играют субъективные факторы?
#question #comparison
Да, это действительно очень мощный подход.
Но, мне кажется, разные языки дают разную поддержку для этого подхода. Т.е., в одних языках проще получается реализовывать свои концепции, а в других — сложней. Один язык/компилятор бьет тебя по рукам, или вынуждает городить длинные конструкции, а другой — даже позволяет стрелять себе в ногу ;)
Наверное, это можно назвать мощностью выразительных средств языка. Как по вашему, возможно ли как-то более-менее объективно упорядочить языки по этой величине?
Или тут больше играют субъективные факторы?
#question #comparison
МБ
「 Есть очень мощный подход: представьте, что уже имеется подходящая нотация для описания решения задачи, далее просто опишите решение. А затем реализуйте и нотацию. 」
Да, это действительно очень мощный подход.
Но, мне кажется, разные языки дают разную поддержку для этого подхода. Т.е., в одних языках проще получается реализовывать свои концепции, а в других — сложней. Один язык/компилятор бьет тебя по рукам, или вынуждает городить длинные конструкции, а другой — даже позволяет стрелять себе в ногу ;)
Наверное, это можно назвать мощностью выразительных средств языка. Как по вашему, возможно ли как-то более-менее объективно упорядочить языки по этой величине?
Или тут больше играют субъективные факторы?
#question #comparison
Да, это действительно очень мощный подход.
Но, мне кажется, разные языки дают разную поддержку для этого подхода. Т.е., в одних языках проще получается реализовывать свои концепции, а в других — сложней. Один язык/компилятор бьет тебя по рукам, или вынуждает городить длинные конструкции, а другой — даже позволяет стрелять себе в ногу ;)
Наверное, это можно назвать мощностью выразительных средств языка. Как по вашему, возможно ли как-то более-менее объективно упорядочить языки по этой величине?
Или тут больше играют субъективные факторы?
#question #comparison
Как нас учит теория категорий и соответствие Карри-Говорда, всё можно записать в терминах функций (комбинаторов).
r
Как нас учит теория категорий и соответствие Карри-Говорда, всё можно записать в терминах функций (комбинаторов).
Но, на практике все не записывают в терминах функций. Операторы, структуры управления — зачем это все? Видимо, так проще записывать и зачитывать )
[upd] Я не имею ввиду, что невозможно записать. А именно, даже имея возможность, чаще все-таки не ограничиваются записью всего только в терминах функций.
[upd] Я не имею ввиду, что невозможно записать. А именно, даже имея возможность, чаще все-таки не ограничиваются записью всего только в терминах функций.