PLT-redex questions

[Jan Sulmont]

Hello!

First I'd like to thank you all for Racket and more specifically PLT-redex (which I am intending  to use I/o to formalise a workable semantics for the Orc language).

I am struggling to understand how to convert a SOS to a Reduction Semantics. if I understood correctly,  SOS labels carry external semantics . Which reduction semantics claims to turn into syntax. 

Like pairing a context with some state -- how should I convey/turn whatever I mean with this state into syntax, so that meaningful  syntactic reduction can happen? 

Anyone could please point me at an example where the grammar has a  pair (context state) production?

Apology in advance for the vagueness of my question -- I feel I fell to understand something :/

Thank you in advance,

Jan

 

[matt...@ccs.neu.edu]

>
> On Mar 8, 2018, at 4:27 PM, Jan Sulmont <moda...@gmail.com> wrote:
>
> Hello!
>
> First I'd like to thank you all for Racket and more specifically PLT-redex (which I am intending to use I/o to formalise a workable semantics for the Orc language).
>
> I am struggling to understand how to convert a SOS to a Reduction Semantics. if I understood correctly, SOS labels carry external semantics . Which reduction semantics claims to turn into syntax.

You may wish to consider formulating a semantics with define-judgment first (not documented in the book but in the docs). You might be able to get a plain SOS semantics that way.

In a sense this question isn’t about Redex but the relationship between different frameworks of formulating a semantics. For some class of cases, this is systematically doable (that’s how I came up with the reduction semantics for h-o imperative generalization of the lambda calculus for example); for others, it is an open question. I know little about Orc and not enough to know which class it falls into.

> Like pairing a context with some state -- how should I convey/turn whatever I mean with this state into syntax, so that meaningful syntactic reduction can happen?
>
> Anyone could please point me at an example where the grammar has a pair (context state) production?

If I understand you correctly, the Redex book covers some of these examples (which we call machines). It might be the best place to get started. I am sure your local university library has a copy (or will get you one).

— Matthias

[Jan Sulmont]

On Mar 8, 2018, at 10:37 PM, matt...@ccs.neu.edu wrote:

On Mar 8, 2018, at 4:27 PM, Jan Sulmont <moda...@gmail.com> wrote:

Hello!

First I'd like to thank you all for Racket and more specifically PLT-redex (which I am intending  to use I/o to formalise a workable semantics for the Orc language).

I am struggling to understand how to convert a SOS to a Reduction Semantics. if I understood correctly,  SOS labels carry external semantics . Which reduction semantics claims to turn into syntax.

You may wish to consider formulating a semantics with define-judgment first (not documented in the book but in the docs). You might be able to get a plain SOS semantics that way.

In a sense this question isn’t about Redex but the relationship between different frameworks of formulating a semantics. For some class of cases, this is systematically doable (that’s how I came up with the reduction semantics for h-o imperative generalization of the lambda calculus for example); for others, it is an open question. I know little about Orc and not enough to know which class it falls into.

Yes I’ve walked through the “Abstracting abstract machines” tutorial, where I thought  moving from judgment to reduction was only easy due to the simplicity of the language under consideration. 

Like pairing a context with some state -- how should I convey/turn whatever I mean with this state into syntax, so that meaningful  syntactic reduction can happen?

Anyone could please point me at an example where the grammar has a  pair (context state) production?

If I understand you correctly, the Redex book covers some of these examples (which we call machines). It might be the best place to get started. I am sure your local university library has a copy (or will get you one).

I’ve purchased my own copy of the Redex book — and am working slowly my way through the 1st part (which I find very useful)

I am neither a student, nor working in the academic.  I  run  Orc in a large production :)

Jan

— Matthias

[matt...@ccs.neu.edu]

> On Mar 8, 2018, at 5:11 PM, Jan Sulmont <moda...@gmail.com> wrote:
>
>>
>> In a sense this question isn’t about Redex but the relationship between different frameworks of formulating a semantics. For some class of cases, this is systematically doable (that’s how I came up with the reduction semantics for h-o imperative generalization of the lambda calculus for example); for others, it is an open question. I know little about Orc and not enough to know which class it falls into.
>>
> Yes I’ve walked through the “Abstracting abstract machines” tutorial, where I thought moving from judgment to reduction was only easy due to the simplicity of the language under consideration.

It is not the simplicity of the language but the nature of the (recursive) evaluation strategy. The uniformity of lambda makes it easy to translate from trees into sequences and to discover what evaluation contexts are and mean.

For an orchestration language or a pi calculus, this is rather different because you want some freedom of moving things around freely.

Years ago we considered supporting sets of terms in redex and that might help with such languages. Right now you have to “mod out” with pattern-matching in Redex (or worse, procedurally if your pattern is highly unusual).

You may wish to look at the work of Tony Garnock-Jones on Syndicate. His language evaluates in a somewhat non-uniform manner and we used structural rules for a while. For his dissertation though he was able to convert it all to reductions (and could state properties more cleanly that way).

>
>>
>>> Like pairing a context with some state -- how should I convey/turn whatever I mean with this state into syntax, so that meaningful syntactic reduction can happen?
>>>
>>> Anyone could please point me at an example where the grammar has a pair (context state) production?
>>
>>
>> If I understand you correctly, the Redex book covers some of these examples (which we call machines). It might be the best place to get started. I am sure your local university library has a copy (or will get you one).
> I’ve purchased my own copy of the Redex book — and am working slowly my way through the 1st part (which I find very useful)
> I am neither a student, nor working in the academic. I run Orc in a large production :)

Can you focus on a small kernel of Orc, something the size of pi or ccs?

— Matthias