Описание тега plt-redex

Описание тега Вопросы с тегом
PLT Redex is a domain-specific language designed for specifying and debugging operational semantics. Given a grammar and the reduction rules, PLT Redex allows interactive exploration of terms and the use of randomized test generation to attempt to falsify properties of a given semantics.
1 ответ

Как реализовать эквикурсивные типы в PLT Redex?

Я полагаю, что я достаточно хорошо понимаю как равно-рекурсивные, так и изорекурсивные типы. Поэтому я пытался реализовать средство проверки типов для ISWIM с равноэккурсивными типами в PLT Redex. Однако я не могу понять, как заставить работать экви…
02 май '16 в 02:47
1 ответ

lisp-"машина: ожидается нарушение контракта: пара? дано: ()" при уничтожении объекта в модели контроля доступа

Напишите процедуру для уничтожения объекта в моей модели контроля доступа и смоделируйте каждую ситуацию. Это мой код (define st1 (term (st 3 2 (,s0 ,s1 ,s2) (,o0 ,o1) ,br ,m1))) (define m1 (term ((,s0 control ,s0) (,s1 (trans ,r1) ,o0) (,s2 ,r2 ,o1…
27 авг '17 в 03:38
0 ответов

Утверждая, что в Redex не существует выхода для суждения

У меня есть отношение, определенное в PLT Redex, которое принимает два входа и выхода. (define-judgment-form L #:mode (Meet I I O) [--------------------------- (Meet xpr xpr xpr)] ) По другому мнению, я хотел бы иметь в качестве побочного условия, ч…
14 дек '18 в 03:49
2 ответа

Что такое "семантика редукции"? Пожалуйста, объясните использование PLT Redex в терминах непрофессионала.

Кто-нибудь, пожалуйста, объясните использование семантики сокращения и переопределения PLT на более простом языке. Благодарю.
27 июл '09 в 13:28
1 ответ

Ракетка, PLT Redex, тест ->E небытие

Я пытаюсь подготовить семантику для языка. Некоторый вывод может привести к "застрявшему" состоянию. Я хочу проверить, какой определенный термин не может быть приведен в состояние "зависания". Можно ли как-то представить это, используя что-то вроде …
03 авг '15 в 12:55
1 ответ

Может ли PLT-Redex моделировать эти функции?

Только начинаю изучать PLT-Redex... Поднимаются два вопроса: Можем ли мы использовать PLT-Redex для моделирования побочных эффектов? Например: простая конструкция приращения i++? Как насчет thread? Все конструкции, представленные до сих пор, не вклю…
14 июл '13 в 18:24
1 ответ

PLT Redex: параметризация определения языка

Это проблема, которая беспокоит меня в течение некоторого времени, и мне интересно, может ли кто-нибудь здесь помочь. У меня есть модель PLT Redex для языка, называемого lambdaLVar, который является более или менее нетипизированным лямбда-исчисление…
03 апр '13 в 23:43
1 ответ

Зачем мне нужны контексты оценки в Redex?

Вполне возможно написать правила оценки для моего языка без использования контекстов оценки. Моя семантика полностью основана на значении и не позволяет продвигать термин внутри лямбд. Несмотря на это, все ресурсы, которые я видел, так или иначе исп…
02 фев '17 в 19:14
1 ответ

Генерация только хорошо типизированных терминов при тестировании семантики с использованием PLT-Redex

Я новичок в ракетке, и я особенно заинтересован в использовании redex. Я сделал небольшую модель для типизированных арифметических выражений, которую можно найти в книге Пирса о типах и языках программирования. Код приведен ниже: https://gist.github…
16 авг '17 в 20:42
1 ответ

plt-redex: замена, избегающая захвата, бесплатно?

Каждый раз, когда я определяю язык в переопределении PLT, мне нужно вручную определять (исключая захват) функцию подстановки. Например, эта модель не закончена, потому что subst не определено: #lang racket/base (require redex/reduction-semantics) (d…
22 дек '16 в 05:52
1 ответ

Многоточие над цитатой в выражении redex

Я пытаюсь определить метафункцию Redex, которая преобразует список пар в список отдельных чисел следующим образом: #lang racket (require redex) (define-language L (e n ((n n) ...) (n ...)) (n number)) (define-metafunction L ((add-up n) n) ((add-up (…
22 янв '16 в 19:40
1 ответ

Вызвать суждение изнутри редукционного отношения

Я работаю над определением языка, который имеет приведение типов и подтипы следующим образом: (define-language base (t ::= int any) (e ::= number (cast t e)) #| stuff ... |#) Я тогда определяю следующую форму суждения по этому: (define-judgment-form…
05 май '16 в 19:01
1 ответ

Попытка определить маленький язык с помощью redex

Я следую учебному пособию по Redex и в то же время строю модель для типизированных арифметических выражений, как это описано в "Типах и языках программирования" Пирса. Я определил синтаксис и систему типов для такого маленького языка, но мне трудно …
15 авг '17 в 11:23
1 ответ

Распечатайте успехи с помощью redex-check

Я использую redex-check для проверки модели относительно другой, и хотел бы видеть промежуточные (успешные) результаты для целей отладки. Наиболее очевидный способ сделать это - распечатать свойство-expr для данного термина в качестве побочного эффе…
20 окт '15 в 19:03
0 ответов

Лучший способ генерировать термины, удовлетворяющие определенным суждениям в Redex

Мне известно о двух попытках Redex по созданию случайных генераторов с ограничениями: redex-check"s #:satisfying-форма (как обсуждено, например, в этой теме). Статья ESOP'15 "Выбор случайных суждений" (есть домашняя страница). Интересно, была ли вто…
15 дек '17 в 16:09
0 ответов

Сокращение Выражение в Java?

Есть ли в Java модуль для определения языка и сокращения выражений в виде модуля PLT/Redex в Racket?
21 апр '15 в 15:32
1 ответ

Редекс не соответствует

Распространенным способом определения семантики является (например): return v if [some other condition] otherwise, return error Например, рассмотрим (define-language simple-dispatch (e ::= v (+ e e)) (v ::= number string) (res ::= e err) (E ::= hole…
08 май '16 в 21:56
0 ответов

Лисп формализует модель Китайской стены

Я хочу формализовать простую модель Китайской стены на основе PLT Redex и Scheme. Но когда я использовал инструмент "шаговый", чтобы визуализировать различные состояния. Произошла ошибка, и я никогда не видел ее раньше. set-min-height method of edit…
30 авг '17 в 22:08
1 ответ

Сравните модель с реализацией в Redex

Я работаю над созданием в Redex модели системы типов, которая также имеет каноническую реализацию. Я хотел бы использовать redex-check для нечеткого тестирования моей модели против фактической реализации. Реализация (с адаптером) может взять мой абс…
19 окт '15 в 17:27
0 ответов

Можно ли реализовать в PLT-Redex выражение, подобное let *?

Недавно я начал использовать PLT-Redex, и мне интересно, может ли кто-нибудь дать мне несколько указаний о том, как реализовать выражение let *, как в Racket. Прямо сейчас я могу писать простые выражения let вроде этого (let (x (+ 2 4)) in (* x 2)) …
21 июл '20 в 11:35