Request for comments: ART on service commitments

Anoma Research Topics
1

Hi everyone,

@jamie and I would like to invite you to review our ART on service commitments. Here is the link to the pdf in Github repo: https://github.com/anoma/202407-message-logic/blob/main/pdfs/main.pdf

The ART corresponds with the two service commitment sessions we hosted at the Hacker House Q3.

We welcome any thoughts/feedback/questions as a reply to this thread.

Best,
Naqib & Jamie

P.S. Naqib is on vacation until October 11th and may reply later than usual.

5 Likes
2

Tagging @cwgoes @degregat @isheff @Jonathan @ray for visibility. Anyone else is of course also welcome to review!

1 Like
3

I read through the paper, and made the following notes. Hopefully you find them useful.

In 5. of Definition 2.1.4, we read β€œβ„•β‰₯0”. Is this different from just β€œβ„•β€? You freely use β€œβ„•β€ in 5. of definition 2.2.1.

The letter 𝛾 is used as a variable for datatypes, but isn’t declared to be a variable for such in definition 2.1.5.

We may freely assume standard function symbols, such as 0, 1, +, βˆ—, and pairing (-, -), with their usual meanings and types

[…]

We may freely assume standard predicate symbols, such as =, <, ≀, tupling
(-, . . . , -) and projections πœ‹π‘– , with their usual meanings. Meaning will always be
clear.

Tupling and projections are functions, not (generally) predicates. It’s not clear to me what they should mean if we tried interpreting them as predicates.

Unless otherwise stated, we will follow a convention that variable symbols named π‘Ž and 𝑏 (like π‘Ž, π‘Žβ€², π‘Ž1, 𝑏′′, and so on) will have a datatype, and variable symbols of the form 𝑐 may have any datatype.

I’m not really sure what this is trying to say. Is it stating that as and bs will always have a fixed datatype given by the context in which they are used, while c will never have such? I also didn’t see anywhere in the paper where c was used as a variable (except for thresholds), so this aside doesn’t seem needed.

f ∈ FSymb to each of which is associated a type type(f) of the form 𝛾 β†’ 𝛾

What is β€œβ†’β€, and where is it? It’s actually used in quite a few places. Obviously, I know it’s a function type, but that’s not declared anywhere, and its semantics is never described. What is β€œtype”; the function you’re applying to f?

an interpretation function 𝜍 (P) : Time β†’ Place β†’ 𝛾 β†’ Bool

[…]

A function 𝜍 (msg) : (N Γ— Place Γ— Place Γ— Data) β†’ Bool.

why is one curried and the other not? Also, some clarification/intuition on why the signature of 𝜍 (msg) looks like that would be good.

  1. πœβ†“π‘› is the model obtained by restricting 𝜍 to times up to and including 𝑛.
  2. πœβ†‘π‘› is the model obtained by restricting 𝜍 to times from 𝑛 onwards.

Does β€œfrom 𝑛 onwards” include 𝑛?

Also, there should be some kind of formal restriction of Time (e.g. that it’s linearly ordered) so that this can always be made sense of. As it stands, you have the naturals as an archetypal example of Time, but the semantics of 𝜍 just says it’s an arbitrary set.

[[{π‘Ž | πœ™}]]𝑛,𝑝,𝜍 = {𝑑 ∈ 𝛼 | 𝑛, 𝑝 ⊨𝜍 πœ™ [π‘Ž:=𝑑]}

Where does 𝛼 come from?

([[𝑑]]𝑛,𝑝,𝜍 ∈ Nβ‰₯#Time)/𝑛, 𝑝 ⊨𝜍 @𝑑 πœ™

This is the middle-right formula of Figure 3. Where does πœ™ come from? If it is free/fresh, etc, that should be stated.

but none of the examples I was given have this form

What a bizarre line to read in a paper. Who gave them to you, and why is that sufficient for dismissal?

𝐡 = {𝑑 ∈ 𝛼 | 𝑛, 𝑝 ⊨𝜍 πœ™ [π‘Ž:=𝑑]} 𝐴 = {𝑑 ∈ 𝐡 | 𝑛, 𝑝 ⊨𝜍 πœ“ [π‘Ž:=𝑑]} #𝐴/#𝐡 β‰₯ π‘Ÿ 𝑛, 𝑝 ⊨𝜍 Ξ π‘Ÿ π‘Ž : πœ™.πœ“

First formula in figure 3
[…]

𝐡 = {𝑑 ∈ 𝛼 | 𝑛, 𝑝 ⊨𝜍 πœ™ [π‘Ž:=𝑑]} and 𝐴 = {𝑑 ∈ 𝛼 | 𝑛, 𝑝 ⊨𝜍 πœ™ [π‘Ž:=𝑑] ∧ πœ“ [π‘Ž:=𝑑]}

in remark 2.3.1. Is that first A supposed to be a subset of B? Is that second A meant not to be a subset of B? If both are correct and equivalent, should the notations be made consistent?

Threshold. To express Ξ π‘Ÿπ‘ πœ™.πœ“ using Ξ π‘Ÿ πœ™.πœ“ , we just write […]

What is n in that formula? Presumably c?

Future work could explore could explore information flow control

Typo.

but usually that a reasonable first approximation to real life

Typo.

…

I think the paper would be improved with some better intuition early on. For example, it doesn’t seem like intuitive, straightforward explanations of @_𝑑 πœ™, in_𝑝(𝑑), or out_𝑝(𝑑) are ever made.

2 Likes
4

Thanks for sharing! I have a few specific copy-editing comments, which I suspect might be easiest to share as comments directly on the document - is that possible? Otherwise, I can write them here, but it will not be quite as efficient.

General comments

  • The introductory content in section 1 is really well-written. Nicely done!
  • Section 2 I’ve pretty much reviewed previously, and have no further comments on.
  • Section 3 is interesting. I agree that we need ways to negotiate and discover service commitments. I am not sure if the flows or data structures here are going to be quite the right fit (and in some cases the data structures are pretty abstract, so it’s not clear exactly what is intended). I don’t think it makes sense to deeply revise this part now, but we should mark it as a topic to discuss when considering subsequent versions of the report, changes to the specs, or other matters.
1 Like
5

Thanks for your feedback @AHart. Tagging @Jamie since most of the questions and comments target section 2 of the report.

@cwgoes I connected the Github repo to this overleaf project. Feel free to share your comments there.

1 Like
6

Thanks - I left a few comments (very minor). I also notice that the application section just before the references is still marked TODO. What are your plans there?

7

Thanks, resolved your points @cwgoes. Regarding the application section, we still have not decided what to do there yet. We were considering the following two options:

  1. Add a small application section to give a more holistic overview of what service commitments are, how they can be applied and why they are useful. This section would basically summarize the discussions/examples in this post.
  2. Remove this section from this report and create a new ART with applications/examples that are more detailed.

Curious to hear your thoughts. Do you have a preference for one of these two options? Perhaps you see a third one that is even better.

1 Like
8

I think (1), if it can be done quickly, would be most optimal here - we don’t immediately need a full additional ART on service commitments - when we figure out more requirements around how to deploy service commitments and what might need to be specified, we can investigate those questions, but we don’t quite need to do so yet.

1 Like
9

Option 1 it is. I don’t think it’s going to be too much work. We basically have to work out one or two examples to help build an intuition.

1 Like
10

Thank you @AHart for your close attention to this document. I have read your comments and acted on all of them. Responses follow below.

In 5. of Definition 2.1.4, we read β€œβ„•β‰₯0”. Is this different from just β€œβ„•β€? You freely use β€œβ„•β€ in 5. of definition 2.2.1.

Same thing. I forgot to add a notation for this. This is now Notation 2.1.2.

The letter 𝛾 is used as a variable for datatypes, but isn’t declared to be a variable for such in definition 2.1.5.

Fixed, thank you.

We may freely assume standard predicate symbols, such as =, <, ≀, tupling
(-, . . . , -) and projections πœ‹π‘– , with their usual meanings. Meaning will always be
clear.

Tupling and projections are functions, not (generally) predicates. It’s not clear to me what they should mean if we tried interpreting them as predicates.

Typo corrected, thank you.

Unless otherwise stated, we will follow a convention that variable symbols named π‘Ž and 𝑏 (like π‘Ž, π‘Žβ€², π‘Ž1, 𝑏′′, and so on) will have a datatype, and variable symbols of the form 𝑐 may have any datatype.

I’m not really sure what this is trying to say. Is it stating that as and bs will always have a fixed datatype given by the context in which they are used, while c will never have such? I also didn’t see anywhere in the paper where c was used as a variable (except for thresholds), so this aside doesn’t seem needed.

Legacy text removed.

f ∈ FSymb to each of which is associated a type type(f) of the form 𝛾 β†’ 𝛾

What is β€œβ†’β€, and where is it? It’s actually used in quite a few places. Obviously, I know it’s a function type, but that’s not declared anywhere, and its semantics is never described. What is β€œtype”; the function you’re applying to f?

This should now be clarified.

an interpretation function 𝜍 (P) : Time β†’ Place β†’ 𝛾 β†’ Bool
[…]
A function 𝜍 (msg) : (N Γ— Place Γ— Place Γ— Data) β†’ Bool.

why is one curried and the other not? Also, some clarification/intuition on why the signature of 𝜍 (msg) looks like that would be good.

Currying now consistent; thanks for pointing this out.

Intuition for signature of 𝜍(msg) inserted in Remark 2.2.2(4).

  1. πœβ†“π‘› is the model obtained by restricting 𝜍 to times up to and including 𝑛.
  2. πœβ†‘π‘› is the model obtained by restricting 𝜍 to times from 𝑛 onwards.

Does β€œfrom 𝑛 onwards” include 𝑛?

Yes it does. Phrasing tweaked to make this clear.

Also, there should be some kind of formal restriction of Time (e.g. that it’s linearly ordered) so that this can always be made sense of. As it stands, you have the naturals as an archetypal example of Time, but the semantics of 𝜍 just says it’s an arbitrary set.

No. Definition 2.1.5(6) identifies time with an initial segment of the natural numbers. Phrasing tweaked and remark 2.1.7(3) added to emphasise this.

[[{π‘Ž | πœ™}]]𝑛,𝑝,𝜍 = {𝑑 ∈ 𝛼 | 𝑛, 𝑝 ⊨𝜍 πœ™ [π‘Ž:=𝑑]}

Where does 𝛼 come from?

It’s the type of a. Fixed, thank you.

([[𝑑]]𝑛,𝑝,𝜍 ∈ Nβ‰₯#Time)/𝑛, 𝑝 ⊨𝜍 @𝑑 πœ™

This is the middle-right formula of Figure 3. Where does πœ™ come from? If it is free/fresh, etc, that should be stated.

To answer the direct question, \phi is a metavariable ranging over predicates – just as in the other rules. The rule is correct as written, but confusing. I tweaked it for clarity.

but none of the examples I was given have this form

What a bizarre line to read in a paper. Who gave them to you, and why is that sufficient for dismissal?

I’ll answer the questions in turn:

  1. You’re right that this turn of phrase would not belong in a paper and thank you for picking up on that – but this isn’t a paper; it’s a draft report for discussion.
  2. Christopher and Naqib.
  3. Nobody’s dismissing anything; on the contrary. Good design is often an exercise in balancing competing needs. The beginning and end of time is notorious for causing difficulties, because β€œyesterday” and β€œtomorrow” don’t have anything to point to. Based on the example service commitments that I was given, I set up the definitions to concentrate pain where it would be least felt. It’s important to signpost
    • what’s been done (everything’s true after the end of time and false before it),
    • why (because this makes the motivating examples work nicely), and
    • where this may lead to dangerous edge cases (example provided that would work poorly, but this seems safe because in practice nobody would want this).

I have slightly rephrased the comment. If you can come up with a realistically useful service commitment of the form β€œif you do something tomorrow then I’ll do something today”, then please let me know.

𝐡 = {𝑑 ∈ 𝛼 | 𝑛, 𝑝 ⊨𝜍 πœ™ [π‘Ž:=𝑑]} 𝐴 = {𝑑 ∈ 𝐡 | 𝑛, 𝑝 ⊨𝜍 πœ“ [π‘Ž:=𝑑]} #𝐴/#𝐡 β‰₯ π‘Ÿ 𝑛, 𝑝 ⊨𝜍 Ξ π‘Ÿ π‘Ž : πœ™.πœ“

First formula in figure 3
[…]

𝐡 = {𝑑 ∈ 𝛼 | 𝑛, 𝑝 ⊨𝜍 πœ™ [π‘Ž:=𝑑]} and 𝐴 = {𝑑 ∈ 𝛼 | 𝑛, 𝑝 ⊨𝜍 πœ™ [π‘Ž:=𝑑] ∧ πœ“ [π‘Ž:=𝑑]}

in remark 2.3.1. Is that first A supposed to be a subset of B? Is that second A meant not to be a subset of B? If both are correct and equivalent, should the notations be made consistent?

Thank you for noting this. Both are indeed correct and equivalent. Equations tweaked in Remark 2.3.1 to make this more clear.

Threshold. To express Ξ π‘Ÿπ‘ πœ™.πœ“ using Ξ π‘Ÿ πœ™.πœ“ , we just write […]

What is n in that formula? Presumably c?

Yes, error corrected, thank you.

Future work could explore could explore information flow control

Typo.

Thank you, fixed.

but usually that a reasonable first approximation to real life

Typo.

Thank you, fixed.

I think the paper would be improved with some better intuition early on. For example, it doesn’t seem like intuitive, straightforward explanations of @_𝑑 πœ™, in_𝑝(𝑑), or out_𝑝(𝑑) are ever made.

You’re right. Detailed explanation inserted in Remark 2.2.5.

2 Likes