Телеграмм чат группы compilerdev страница 1254

https://github.com/sequents/code/tree/master/src/Lambda/STLC

GitHub

sequents/code

Contribute to sequents/code development by creating an account on GitHub.

много TLA но куда именно смотреть?

16:20пожаловаться #1

Term и Smallstep

16:20пожаловаться #2

там еще парсер, тайпчекер и пачка АМ

16:21пожаловаться #3

https://github.com/sequents/code/blob/master/src/Lambda/STLC/Smallstep.idr#L23 вот это да?

16:22пожаловаться #4

ок, спасибо, буду изучать

16:22пожаловаться #5

это подстановка, сами интерпретаторы отсюда https://github.com/sequents/code/blob/master/src/Lambda/STLC/Smallstep.idr#L51

16:22пожаловаться #6

первый call-by-name, второй call-by-value

16:23пожаловаться #7

каждая строчка по сути и есть правило переписи

16:23пожаловаться #8

баяны [| foo (f x) (g y) |] это грубо говоря сахар для чего то типа

if f x is Just x' then 
  if g y is Just y' then 
    Just foo x' y' 
  else Nothing

16:25пожаловаться #9

это нужно для поиска редексов внутри терма

Igor 🐱 Jirkov in Compiler Development

16:26пожаловаться #10

мелкошаговый совсем автоматный, а крупношаговый ближе к денотационной семантике, он более абстрактный, т.е. оставляет технические вещи за кадром отчасти

Я долгое время не понимал разницу. В моей голове сложилась такая интуиция: результат выполнения программы в small step — трейс состояний/событий, а в big step — скажем, число

16:33пожаловаться #11

заканчивается тогда когда заканчиваются правила :)

про составление правил для оп семантики - вот например у нас есть какой-то general purpose язык, как мы составляем для него опсем правила и где там заканчиваются правила?

16:35пожаловаться #12

Igor 🐱 Jirkov

ну да, бигстеп схлопнет всю цепочку редукции до одной реляции

16:36пожаловаться #13

Berkus Decker

заканчиваются в смысле "больше нечего применять"

16:38пожаловаться #14

как составляем - ну это как в любом моделировании, смотрим на те свойства которые нам интересны и следим чтобы модель адекватно отображала то что в языке происходит

16:38пожаловаться #15

есть всякие инструменты, упрощающие этот процесс, например https://redex.racket-lang.org/

16:39пожаловаться #16

заканчиваются в смысле "больше нечего применять"

да, но должны быть какие-то критерии что мы должны получить на выходе правил же, что там получается то?