Notation for terms/processes in CS calculi

Stream: computer science

[Fabrizio Montesi]

(Spin-off of #general > Lambda calculus)

We're gonna be full of reduction and transition relations for operational semantics in https://github.com/cs-lean/cslib (we already have the one for CCS, and people are working on lambda calculus, SKI, and pi-calculus already). I'm trying to make sense of how to give all these semantics the expected notation.

All these relations typically have the notation m → n, sometimes with a label on top, sometimes with a subscript on the arrow, plus the accompanying notation m ⇒ n for the derived 'saturated' version (given by the reflexive and transitive closure of →). In our research group we've been using -[l]-> for a transition with label l, which would then give =[l]=> for the saturated variant.

Another thing to consider is that one syntax can have many accompanying definitions of semantics. For example, the lambda calculus has a lot of possible evaluation strategies (like cbv and cbn), with more being developed. The study of structural operational semantics and mathematical semantics made some languages have both a reduction and a transition semantics, etc.

A solution could be to define typeclasses for the different classes of reduction/transition relations, and make the notation parameterised on the name of the relation.

For example, if cbv : Term -> Term -> Prop, we instantiate something like Semantics.IsReductionRelation and now we can write m →cbv n. Would that be ok?

Some languages are lucky, like CCS has essentially one lts semantics. For these situations we could have a typeclass that does not require specifying the name of the relation.

@Chris Henson @Thomas Waring @Yicheng Qian

[Thomas Waring]

Fabrizio Montesi said:

All these relations typically have the notation m → n, sometimes with a label on top, sometimes with a subscript on the arrow, plus the accompanying notation m ⇒ n for the derived 'saturated' version (given by the reflexive and transitive closure of →).

In my development of SKI I have used . ⇒ . for single-step reduction, and . ⇒* . for its reflexive-transitive closure. I'm not totally wedding to this, but I avoided . → . to avoid mixing it up with the functional arrow: for instance a transitive law
(a → b) → (b → c) → (a → c)
would certainly confuse me, even if lean would parse it correctly. While maybe not universal the * for multi-step reduction is familiar to me, and makes sense by (rough) analogy with the Kleene star.

[Fabrizio Montesi]

The Kleene star after the arrow is used in a lot of papers, I like it myself. Also because you can then do ->+ for the version that requires at least one step. And your choices certainly make sense I'm the local context of SKI.

But in LTSs, the => typically means closure on tau-transitions.

I'm gonna try to make a file that gives an overview of all notations at a glance and possible conflicts, maybe that'll facilitate the discussion. Maybe it's a pipedream to have one convention, but I'd like to make sure. :⁠-⁠)

[Fabrizio Montesi]

Oof, there's no unicode symbol for a two-headed double arrow, right? :(
I want ⇒ with a double head, as in ↠.

[Aaron Liu]

➾

[Aaron Liu]

It's "U+27BE OPEN OUTLINED RIGHTWARDS ARROW"

[Aaron Liu]

shows up as a double headed double arrow on my font

[Fabrizio Montesi]

Ok, I see two options for all our nice arrows. I've summarised them here: https://github.com/cs-lean/cslib/blob/main/NOTATION.md

Basically, Option A uses an extra arrow head to mean 'possibly multiple steps', whereas Option B uses the Kleene star. I used Option A in my textbook on choreographic programming because having a * in addition to transition labels looked cumbersome, but I'm not married to this.

Are there more options that I've missed maybe?

I'm not really happy with m →[cbv] n and p [μ]→[late] q when we mention the relation explicitly, but I couldn't figure anything better out yet.. :-)

[Fabrizio Montesi]

(Maybe just get rid of the square brackets?..)

[Aaron Liu]

get rid of which square brackets

[Aaron Liu]

the brackets are to help everyone figure out how everything is bracketed

[Fabrizio Montesi]

The ones around cbv, or late, or \mu.

[Fabrizio Montesi]

Aaron Liu said:

the brackets are to help everyone figure out how everything is bracketed

I put them there! But I also feel like it's getting a bit busy (the notation).

[x.y.]

Fabrizio Montesi said:

Ok, I see two options for all our nice arrows. I've summarised them here: https://github.com/cs-lean/cslib/blob/main/NOTATION.md

Basically, Option A uses an extra arrow head to mean 'possibly multiple steps', whereas Option B uses the Kleene star. I used Option A in my textbook on choreographic programming because having a * in addition to transition labels looked cumbersome, but I'm not married to this.

Are there more options that I've missed maybe?

I'm not really happy with m →[cbv] n and p [μ]→[late] q when we mention the relation explicitly, but I couldn't figure anything better out yet.. :-)

I especially find p [μ]→[late] q being a bit hard for my brain to parse, as μ (transition label) and late(type of transition/semantics) are different things but written in the same brackets... Although things like p [μ]→(late) q or p [μ]→<late> q are busier and probably harder to read...

[Fabrizio Montesi]

Mmmh right.. so at least the square brackets around the \mu should probably go.

[Fabrizio Montesi]

@Thomas Waring I agree that looking at the same arrow in implications about transitions is gonna be a bit weird and tried to do something about it, but it soon became a lost cause once I started thinking about type systems and logics (which are gonna use the same arrow..).
What do you think of the current proposals? Could you live with both/one/none of them? I'm still very much in doubt about brackets, at least. (Tempted to remove them altogether.)

In the meantime I'm reviewing the rest of your SKI pr. :-⁠)

[Thomas Waring]

For my part those logical / type system examples are less egregious, since there at least the arrow has (more-or-less) the same semantics — ie we aren't mixing up "arrow as transition" and "arrow as function". If it becomes a problem syntactic implication is sometimes written "$\supset$" to distinguish it from implication "in the meta".

That being said I could certainly live with your proposals, with a preference for the second (Kleene star) version — to me a double headed arrow means "surjection", though I could certainly get used to it. I would vote to keep the brackets, but possibly that's because so far I haven't had to use them...

[Fabrizio Montesi]

I see your points. I slightly prefer the extra arrow head because it takes a symbol away, the notation can get super busy.. like p μs⇒late* q

[Fabrizio Montesi]

Btw, done reviewing the ski pr. We can merge it before we're done with this discussion, as long as notation is locally scoped. Between SKI and CCS, we actually already hit all the use cases for the notation. For example, you already have an alternative semantics (parallel reduction). In my proposal it'd read something like p →par q. It'd be great if we could somehow choose how we annotate the arrow when we instantiate the relation, so that one could write the p-subscript as you do and link it to ParallelReduction. This goes beyond my notation-fu though.... :thinking:

[Fabrizio Montesi]

Ah, well, I guess one could make it work with abbreviations, giving other names to the relations.

[Chris Henson]

@Fabrizio Montesi To clarify, you want that when we define a relation, we select what name it uses in conjunction with arrow for notation? I think I can write this, either as an attribute or command you run afterwards. I think it would be good that this also does so for the reflexive (symmetric) transitive closures since they are common.

[Fabrizio Montesi]

Chris Henson said:

Fabrizio Montesi To clarify, you want that when we define a relation, we select what name it uses in conjunction with arrow for notation? I think I can write this, either as an attribute or command you run afterwards. I think it would be good that this also does so for the reflexive (symmetric) transitive closures since they are common.

Yes that's the idea. An attribute/command thing would be awesome.

[Thomas Waring]

Fabrizio Montesi said:

I see your points. I slightly prefer the extra arrow head because it takes a symbol away, the notation can get super busy.. like p μs⇒late* q

this is a good point (as I discovered when I tried to work with multi-step reduction on polynomials ⇒'*

[Thomas Waring]

Fabrizio Montesi said:

Btw, done reviewing the ski pr.

thanks for your comments! i've committed the suggested changes to names, and making notation scoped to the SKI namespace. I've also made an effort to name lemmas about say MRed (multi-step reduction) as MRed.[...] — is this appropriate? (Excuse my lean newbie questions!)

[Chris Henson]

I asked a question in #metaprogramming / tactics > defining notations with an attribute about defining notations with attributes. Either way, I think the command version works and would help to unify notation.

(The arrows and precedence I used there were arbitrary, I do not have too strong an opinion.)

[Fabrizio Montesi]

Thomas Waring said:

Fabrizio Montesi said:

Btw, done reviewing the ski pr.

thanks for your comments! i've committed the suggested changes to names, and making notation scoped to the SKI namespace. I've also made an effort to name lemmas about say MRed (multi-step reduction) as MRed.[...] — is this appropriate? (Excuse my lean newbie questions!)

Yes! And, merged! :smiley:

[Fabrizio Montesi]

Chris Henson said:

I asked a question in #metaprogramming / tactics > defining notations with an attribute about defining notations with attributes. Either way, I think the command version works and would help to unify notation.

(The arrows and precedence I used there were arbitrary, I do not have too strong an opinion.)

Looking good, let me know when you figure out the attribute thing.

I'm also thinking about how we can deal with reductions more uniformly. We could do it as I did for LTS, that is, define a ReductionSystem structure that takes a red relation field. Then, we can make a file for ReductionSystem that automatically gives mred, mred.single, etc. See https://cs-lean.github.io/Cslib/Semantics/LTS/Basic.html

Then we could make all sorts of notation tricks for ReductionSystem and LTS.

Maybe a structure is overkill and it could just be an abbreviation, or it could be a Relation or CRel... Not sure about this specific bit since that discussion is still pending in mathlib.

[Fabrizio Montesi]

Hopefully this can be done without creating any or too much friction in reusing the results about Relation and such.

[Fabrizio Montesi]

It's really cool that we have already covered enough languages/semantics to play with this tbh!

[Chris Henson]

@Fabrizio Montesi I have opened a PR with the proposed attribute: https://github.com/cs-lean/cslib/pull/9

As I say in the description, we probably want different arrows than the ones I used there, it is easily changed.

[Fabrizio Montesi]

Super, thanks!

What's the interest in deriving an equivalence relation out of a reduction semantics through EqvGen, in general?

[Chris Henson]

If I am talking about a semantics being sound wrt to a reduction, it is not uncommon to talk about this equivalence relation. For proofs of confluence, normalization, etc. we probably only care about the reflexive transitive closure, but I don't think it hurts to reserve the notation.

[Fabrizio Montesi]

Do you have a reference for that? I vaguely recall something like that from rewriting systems maybe?..

[Fabrizio Montesi]

In the meantime I made my idea formal, see https://github.com/cs-lean/cslib/blob/main/Cslib/Semantics/ReductionSystem/Basic.lean
It has a similar API to LTS.
An LTS is instantiated like this: https://github.com/cs-lean/cslib/blob/9311d10dac269c8d5b097c41eef78f5b07b6a238/Cslib/ConcurrencyTheory/CCS/Semantics.lean#L37
We could do the same, e.g., in SKI @Thomas Waring. That is, right after defining Red, we could:

def rs : ReductionSystem SKI where
  Red := Red

And rs would now immediately have both rs.Red and rs.MRed, along with any general useful theorem we can think about for them (I've put a couple), just like in CCS lts gets immediately lts.Tr, lts.MTr, and lts.STr.

What do you think? I'm not exactly sure where we should instruct the notation with this approach. The definition of rs maybe?

[Fabrizio Montesi]

(@Thomas Waring I've added your name as an author to that file because I copy-pasted some stuff from your SKI semantics, let me know if you're not ok with that)

[Fabrizio Montesi]

I've also added Option C for notation, for using triangle heads instead of normal arrows. Does that look better?

https://github.com/cs-lean/cslib/blob/main/NOTATION.md

[Thomas Waring]

That all seems reasonable to me :-)

[Chris Henson]

Fabrizio Montesi said:

Do you have a reference for that? I vaguely recall something like that from rewriting systems maybe?..

Yes, rewriting systems. For instance see Term Rewriting and All That.

[Chris Henson]

Fabrizio Montesi said:

I've also added Option C for notation, for using triangle heads instead of normal arrows. Does that look better?

https://github.com/cs-lean/cslib/blob/main/NOTATION.md

I have a preserence for not trying to use the same arrow for implication. I would personally mix A and B and use m ⭢ n for reduction and m ↠ n for multistep (reflexive transitive closure).

[Chris Henson]

Fabrizio Montesi said:

What do you think? I'm not exactly sure where we should instruct the notation with this approach.

The paramaterized notation still works fine with ReductionSystem, it would just define this structure. Should I update my PR to do this?

[Chris Henson]

Maybe ReductionSystem should have a field for the suffix symbol we use with the arrow? What do you think?

[Fabrizio Montesi]

Chris Henson said:

Maybe ReductionSystem should have a field for the suffix symbol we use with the arrow? What do you think?

How would that look like/work?
An alternative is that we annotate the definition of the reduction system, so that the user can control the notation generated for it I guess?

[Chris Henson]

I meant that we have

structure ReductionSystem (Term : Type u) where
  Red : Term → Term → Prop
  suffix : String -- maybe not actually String, the type for notation

and define the notations for ReductionSystem.Red and ReductionSystem.MRed. Storing this is maybe not strictly necessary, but could be nice to have this recorded wthin this API structure.

We could still use the attribute when defining a reduction, e.g. write

@[reduction "ᶜ"]
inductive Red : SKI → SKI → Prop where ...

and it defines the ReductionSystem SKI.

[Chris Henson]

(Btw I have a branch with confluence for the locally nameless presentation about ready to PR, I am going to wait until we settle this reduction notation so it uses the API we settle on)

[Fabrizio Montesi]

Chris Henson said:

I meant that we have

structure ReductionSystem (Term : Type u) where
  Red : Term → Term → Prop
  suffix : String -- maybe not actually String, the type for notation

and define the notations for ReductionSystem.Red and ReductionSystem.MRed. Storing this is maybe not strictly necessary, but could be nice to have this recorded wthin this API structure.

We could still use the attribute when defining a reduction, e.g. write

@[reduction "ᶜ"]
inductive Red : SKI → SKI → Prop where ...

and it defines the ReductionSystem SKI.

Ah, I see! I'd avoid mixing data with notation for now, but let's keep this in mind as a later option in case it becomes relevant.

For the annotation, I see two options (we can change the concrete annotation names, it's just an example). In your proposal, I guess we'd need to add the name of the ReductionSystem.

For example,

@[derive_reduction_system rs "ᶜ"]
inductive Red : SKI → SKI → Prop where ...

would define a ReductionSystem called rs with notation suffixed by c.
Otherwise, we could write

@[notation_name "ᶜ"]
def rs : ReductionSystem SKI where ..

The two could even coexist (the first could be a macro for the second).

[Fabrizio Montesi]

What's the casing one should use for annotations, btw? camelCase, I guess?

[Fabrizio Montesi]

Are there other annotations like this that we could take some inspiration from regarding the names of all these?

[Chris Henson]

This seems good to me! We could derive the name of the reduction system, but probably better to have it explicit. I'll give this a try.

[Chris Henson]

Fabrizio Montesi said:

What's the casing one should use for annotations, btw? camelCase, I guess?

I'm not sure where it's documented, but every attribute I've seen is lower snake case.

[Fabrizio Montesi]

Huh, I hadn't thought about it, but would it be an option to use deriving clauses right after the definition of reduction relations for the same purposes?

https://lean-lang.org/doc/reference/latest/Type-Classes/Deriving-Instances/

[Chris Henson]

I considered this, but I wasn't sure if it was idiomatic because of the argument for the suffix. I could try it and see what we prefer.

[Chris Henson]

For now, I have pushed an update that makes the notation attribute use ReductionSystem. I left a couple of comments on things I wasn't sure about.

[Chris Henson]

Yeah, I could be wrong, but I'm not seeing a way to pass in a parameter like that.

[Fabrizio Montesi]

Chris Henson said:

Fabrizio Montesi said:

I've also added Option C for notation, for using triangle heads instead of normal arrows. Does that look better?

https://github.com/cs-lean/cslib/blob/main/NOTATION.md

I have a preserence for not trying to use the same arrow for implication. I would personally mix A and B and use m ⭢ n for reduction and m ↠ n for multistep (reflexive transitive closure).

Why mix two different arrow heads? (I don't have a strong opinion.)

[Fabrizio Montesi]

Chris Henson said:

For now, I have pushed an update that makes the notation attribute use ReductionSystem. I left a couple of comments on things I wasn't sure about.

This looks very good to me. :-)
I'd put this directly in ReductionSystem.lean and call the annotation reduction_sys or gen_reduction_sys (since it creates a reduction system).
Could I also ask for the same stuff for LTSs? (same terminology, so either lts or gen_lts)

[Chris Henson]

I moved this into the ReductionSystem file and used the name reduction_sys for the attribute. I didn't have a deep thought about the arrows, those just seemed like the ones closest to what we write on paper.

Can you point out exactly which LTS types should be used in the reduction notations? Attributes need to be defined in their own file before they are used, so we might need move a couple of things.

[Fabrizio Montesi]

In Semantics/LTS/Basic.lean, type LTS corresponds to ReductionSystem. The only difference is that LTS takes a Tr relation of type State -> Label -> State -> Prop, instead of a Red : Term -> Term -> Prop relation. (State is like Term.)

So what is needed is annotating the def of a relation like Tr : State -> Label -> State -> Prop relation, much like we annotate the def of a reduction relation Red : Term -> Term -> Prop. That should def an LTS, just like we currently def a ReductionSystem.

See CCS/Semantics.lean for an example where I do it manually.

[Chris Henson]

Okay, I'll take a look. I'm having a seperate issue I need to fix first with inferring type variables. This wasn't a problem when working with Relation.ReflTransGen directly, I'll have to think a bit...

[Chris Henson]

@Fabrizio Montesi I have added the attribute notation for LTS. I used it in the file CCS/Semantics.lean you meantioned and in a test to confirm it is working, even with variables (thanks to Kyle Miller!).

[Fabrizio Montesi]

It looks great!

Mini questions:

• Sometimes there's a canonical semantics, e.g., in CCS the LTS I've defined is widely accepted as 'the one'. I guess I could just pass an empty string as the suffix for the arrow and it'd work? Maybe if things get more complex in the future we could make actual named parameters (like in aesop), but we can always do that later.
• If one annotation is 'reduction_sys', the other should just be 'lts'. Otherwise, both should have the 'gen' prefix. I'm fine with both options, just wanted to point out the current inconsistency.

[Chris Henson]

• An empty string does not currently work, but I should be able to easily make it so that if you don't pass a string it defines the cannonical notation
• I will change the name for consistency

[Fabrizio Montesi]

Forgot to say: I'd also get rid of the square brackets around transition labels. I think most people are gonna write round parentheses when it matters.

I can do that bit myself if you like, I'll play a bit with CCS.

[Chris Henson]

I have pushed those two changes. Yes, please feel free to change the notation. I went with the square bracket simply because I was getting confused by precedence while also trying to figure out the metaprogramming stuff.

[Fabrizio Montesi]

Merged! Thanks for this lovely notation-fu. :⁠-⁠) I'll play with it as soon as I have time.

[Chris Henson]

Nice, thanks! This was a great way for me to learn some more metaprogramming. I will use it for my upcoming confluence PR as well.

[Fabrizio Montesi]

@Thomas Waring Does the ReductionSystem thing work for your SKI formalisation?

[Notification Bot]

This topic was moved here from #general > Notation for terms/processes in CS calculi by Bryan Gin-ge Chen.

[Thomas Waring]

This looks great! & it seems like it ought to work for SKI, but I'm having a little trouble making it match up — for example in the following

lemma parallel_mRed {a a' b b' : SKI} (ha : a ↠ a') (hb : b ↠ b') :
    (a ⬝ b) ↠ (a' ⬝ b') :=
  Trans.simple (rs.MRed.head b ha) (rs.MRed.tail a' hb)

I get an error saying failed to synthesize Trans rs.MRed rs.MRed rs.MRed, which looks verbatim like something in ReductionSystem.Basic.lean

[Thomas Waring]

Similarly if I replace the above by a calc block I get

'calc' expression has type
  Relation.ReflTransGen rs.MRed (a ⬝ b) (a' ⬝ b') : Prop
but is expected to have type
  rs.MRed (a ⬝ b) (a' ⬝ b') : Prop

[Thomas Waring]

Am I using it correctly? I've open -ed Red and ReductionSystem, and used a an unlabelled arrow

[Bhavik Mehta]

Thomas Waring said:

This looks great! & it seems like it ought to work for SKI, but I'm having a little trouble making it match up — for example in the following

lemma parallel_mRed {a a' b b' : SKI} (ha : a ↠ a') (hb : b ↠ b') :
    (a ⬝ b) ↠ (a' ⬝ b') :=
  Trans.simple (rs.MRed.head b ha) (rs.MRed.tail a' hb)

I get an error saying failed to synthesize Trans rs.MRed rs.MRed rs.MRed, which looks verbatim like something in ReductionSystem.Basic.lean

It looks like

Trans MRed MRed MRed

is missing (and necessary)

[Bhavik Mehta]

You have three Trans instances, but you need four, like this: https://gist.github.com/b-mehta/e412c837818223b8f16ca0b4aa19b166#file-sk_calculate-lean-L76

[Thomas Waring]

Ah you're absolutely right, thanks

[Chris Henson]

@Thomas Waring Is this in a branch I could look at? I am able to #synth Trans rs.MRed rs.MRed rs.MRed for any of the other reduction systems. Or just mention it at this issue when this ends up in a PR so we can coordinate any changes about Trans instances.

[Chris Henson]

@Thomas Waring Looking at your messages closer I realize this is probably because of the bad instances Trans R R (ReflTransGen R) and Trans rs.Red rs.Red rs.MRed mentioned in the issue I linked above. I have another PR removing it, but you can give ahead and do so in your branch too and it should fix the issue.

[Thomas Waring]

Okay great, as it is I fixed made it work using these instances:

instance (rs : ReductionSystem Term) : IsTrans Term rs.MRed := by infer_instance
instance (rs : ReductionSystem Term) : Transitive rs.MRed := transitive_of_trans rs.MRed
instance (rs : ReductionSystem Term) : Trans rs.MRed rs.MRed rs.MRed := instTransOfIsTrans

though I expect some of them would be redundant

[Thomas Waring]

I've got everything working at https://github.com/thomaskwaring/cslib_SKI, but I'd appreciate your giving it a once over to check whether I'm using everything correctly

[Thomas Waring]

Though I guess that could just be a PR?

[Thomas Waring]

Also, (somewhat) silly question, is there a vscode shortcut for the single-step arrow?

[Fabrizio Montesi]

Thomas Waring said:

Also, (somewhat) silly question, is there a vscode shortcut for the single-step arrow?

No but I was thinking about the same. I suggest we use '\tr' and '\mtr' (for transition and multistep transition, respectively), and if you like we can have also '\red' and '\mred' for the same symbols.

[Thomas Waring]

either / both works for me :)

[Fabrizio Montesi]

Btw, I'm encountering similar problems for LTSs. I managed to instantiate a Trans that should be useful (more coming later once I fix this one..):

instance (lts : LTS State Label) : Trans (fun s1 => lts.Tr s1 μ1) (fun s2 => lts.Tr s2 μ2) (fun s3 => lts.MTr s3 [μ1, μ2])

But calc isn't happy, it thinks there's a mismatch between the output and input type of the two equations that you can find in my commented examples at the bottom here:

https://github.com/cs-lean/cslib/blob/931d29d60ea5bc3492cd953fa7f63853a1796b09/CslibTests/CCS.lean#L18

Any ideas about what I'm doing wrong?

[Fabrizio Montesi]

Thomas Waring said:

either / both works for me :)

Added. :)

[Chris Henson]

Thomas Waring said:

Though I guess that could just be a PR?

Seems good to me, and I can look again when there's a PR. I will look closer again at the instances when we bump Mathlib and pick up what I upstreamed. Maybe I wait until after this PR then do this?

[Fabrizio Montesi]

Chris Henson said:

Thomas Waring said:

Though I guess that could just be a PR?

Seems good to me, and I can look again when there's a PR. I will look closer again at the instances when we bump Mathlib and pick up what I upstreamed. Maybe I wait until after this PR then do this?

We're kinda stuck bumping mathlib because of the unfinished Rel discussion. Maybe we should just bite the bullet and drop using Rel altogether?

[Fabrizio Montesi]

The code about behavioural equivalences like bisimilarity would get ugly though, I'm afraid. :⁠-⁠|

[Fabrizio Montesi]

Though maybe it's just a matter of finding good notation for inv, comp, and upTo.

[Chris Henson]

Yeah from following that conversation at a distance, I think the solution is API like this that abstracts away from the abbrev not being what you'd prefer. I'm really sold on this pattern since it simplified so many proofs in my last PR.

[Fabrizio Montesi]

What pattern are you referring to? Drop having an abbreventirely and just make our own notation when needed?

[Chris Henson]

I mean how in my last PR how I changed to never destructing the notations for opening, closing, or substitution. I don't really care what the underlying type is, because I have a bunch of little lemmas about the notation instead. Maybe the situation could be similar here?

[Thomas Waring]

@Chris Henson you mentioned the precedence for reduction notation wasn't fixed, I'm finding myself writing things like ¬ (x ⭢ y), (P ⬝ x ↠ TT) ∨ P ⬝ x ↠ FF, etc a bit, perhaps it would make sense if it had higher precedence than logical connectives?

[Chris Henson]

Thomas Waring said:

Chris Henson you mentioned the precedence for reduction notation wasn't fixed, I'm finding myself writing things like ¬ (x ⭢ y), (P ⬝ x ↠ TT) ∨ P ⬝ x ↠ FF, etc a bit, perhaps it would make sense if it had higher precedence than logical connectives?

Yes, feel free to change the precedence, I'm not good at selecting those. If you do, please change both LTS and ReductionSystem for consistency.

[Fabrizio Montesi]

Fabrizio Montesi said:

Btw, I'm encountering similar problems for LTSs. I managed to instantiate a Trans that should be useful (more coming later once I fix this one..):

instance (lts : LTS State Label) : Trans (fun s1 => lts.Tr s1 μ1) (fun s2 => lts.Tr s2 μ2) (fun s3 => lts.MTr s3 [μ1, μ2])

But calc isn't happy, it thinks there's a mismatch between the output and input type of the two equations that you can find in my commented examples at the bottom here:

https://github.com/cs-lean/cslib/blob/931d29d60ea5bc3492cd953fa7f63853a1796b09/CslibTests/CCS.lean#L18

Any ideas about what I'm doing wrong?

Update: I've made calc work with LTS. :) But in doing so I've realised something else (next mesg).

[Fabrizio Montesi]

While we have notation for _specific_ LTSs and reduction systems now, we don't have a notation for those in general. For example, I cannot use the transition notation in this definition:

def Bisimulation (lts : LTS State Label) (r : State → State → Prop) : Prop :=
  ∀ s1 s2, r s1 s2 → ∀ μ, (
    (∀ s1', lts.Tr s1 μ s1' → ∃ s2', lts.Tr s2 μ s2' ∧ r s1' s2')
    ∧
    (∀ s2', lts.Tr s2 μ s2' → ∃ s1', lts.Tr s1 μ s1' ∧ r s1' s2')
  )

[Fabrizio Montesi]

I guess such a notation would need to mention lts somewhere, as I do in the notation for bisimilarity (s ~[lts] s').

[Chris Henson]

What happens if have a variable for lts and add the attribute to it? Not sure how the scoping works when you then use this in another file.

[Fabrizio Montesi]

No idea, that sounds... interesting? dangerous? :-)

[Fabrizio Montesi]

I've tried but didn't manage to use the variable trick. I can't seem to be able to add the attribute (which makes sense).

[Fabrizio Montesi]

Working with dfas is making this even more painful. Would be nice to have theorems about transition systems stated with the notation, instead of Tr, MTr, etc. :-\