Allow partial signatures in agent declaration

[jkrivine]

If one interprets signatures as types for rules (a la Russ), then I believe one should allow for partial signatures. For instance %agent: A(x!x.B) %agent: B(x)

should be a correct type for A(x),B(x) -> A(x!1),B(x!1)

[pirbo]

You're right, that's why it is already implemented!

%agent: A(x!x.B)
%agent: B(x)

fails though as you don't say that B.X can binds A.x

%agent: A(x!x.B)
%agent: B(x!x.A)

is correct.

Le 28 juin 2017 à 05:55, Krivine [email protected] a écrit :

If one interprets signatures as types for rules (a la Russ), then I believe one should allow for partial signatures. For instance %agent: A(x!x.B) %agent: B(x)

should be a correct type for A(x),B(x) -> A(x!1),B(x!1)

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub, or mute the thread.

[jkrivine]

I don't understand. If I write %agent: A(x) This does not mean that A cannot bind B on x right? So I don't understand why %agent: A(x!x.B) %agent: B(x) should fail

[pirbo]

Agent déclaration is not compositionnable:

• As soon as you declare 1 agent, you have to declare them all and
• As soon as you give the "contact map" of 1 site of 1 agent, you have to give the one of all the site of all the agents. Any other convention I can imagine would be a nightmare to implement but help yourself if you have an idea...

[pirbo]

@jkrivine: Alors, qu'est qu'on fait ?

[jkrivine]

Here is a suggestion:

[1] We need a special symbol for "free", let us say "A(x!*)" and here A(x) means the old symbol A(x?) [2] We define two sorts of interfaces for the link state:

the Complete interface type of the form

%agent: A(x!<y.B,z.C,t.D,*>)

and partial interface of the form

%agent: A(x!*!x.A!x.B...)

The interpretation of A(x!<y.B,.>) is that A can either be free () or bound to y of B In particular A(x!<*>) imposes that x remains always unbound

[3] Now we can introduce subtyping for the partial interfaces: A(x\sigma) < A(x\sigma!y.B)

where in particular A(x) is a subtype of A(x!y.A)

Now A(x!y.A) should raise a warning if no rule implements that link A(x!<y.A,*>) raises an error if no rule implements the link

Le 28/06/2017 à 12:04, Pierre Boutillier a écrit :

You're right, that's why it is already implemented!

%agent: A(x!x.B)
%agent: B(x)

fails though as you don't say that B.X can binds A.x

%agent: A(x!x.B)
%agent: B(x!x.A)

is correct.

Le 28 juin 2017 à 05:55, Krivine [email protected] a écrit :

If one interprets signatures as types for rules (a la Russ), then I believe one should allow for partial signatures. For instance %agent: A(x!x.B) %agent: B(x)

should be a correct type for A(x),B(x) -> A(x!1),B(x!1)

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub, or mute the thread.

— You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub https://github.com/Kappa-Dev/KaSim/issues/409#issuecomment-311615699, or mute the thread https://github.com/notifications/unsubscribe-auth/AAR5ji6AOM1fkt3852-VVNBsDmy9VhKfks5sIiVHgaJpZM4OHvgZ.

-- Chargé de recherche à l'IRIF Équipe PPS - Univ. Paris Diderot +33 1 57 27 93 38

[pirbo]

All the pieces to do it are now there. It would be boring but straightforward. I don't see the point enough to get the motivation. Help yourself :-)