[ontoiop-forum] DOL finalisation

[Till Mossakowski]

Rick,

Am 04.01.2018 um 22:29 schrieb rick:
> Thanks Till, but I don't get it.
>
> I read section 2.2 and Definition 2 clause 10, but no institution was
> presented in the proposal to justify your claim, right? If so, where is it?
I can just repeat myself: the fact that a particular institution does
not appear in the DOL standard does not entail that it is outside the
scope of DOL.
>
> While institutions are broadly applicable, the RFP restricts DOL scope
> and conformance to 6.5.5. Second order logic is not included in 6.5.5
> and its not in the proposal.
Right, second-order logic is not mentioned in the standard. Still, it is
within the scope of DOL. See section 2.2 "Conformance of an OMS
Language/a Logic with DOL", which basically entails that any institution
is within the scope of DOL.
>
> Also, if there's no institution-theoretic work on System F, there can't
> be, right?
I would not draw this conclusion.
That said, indeed polymorphism is difficult to capture as an
institution, because the satisfaction condition (the only, rather mild,
condition governing institutions) easily fails if you do not take care.
See [1].

Best, Till

[1] Lutz Schröder, Till Mossakowski and Christoph Lüth. Type class
polymorphism in an institutional framework. In: J. Fiadeiro, editor,
Recent Trends in Algebraic Development Techniques, 17th International
Workshop (WADT 2004), volume 3423, series Lecture Notes in Computer
Science, pages 234-248. Springer; Berlin; http://www.springer.de, 2005.

>
> --
> Rick
>
> On 01/03/2018 03:00 PM, Till Mossakowski wrote:
>> Rick,
>>
>> Am 03.01.2018 um 20:34 schrieb rick:
>>> Dear Till,
>>>
>>> Thanks so much for pointing this out. See below.
>>>
>>> On 01/02/2018 05:33 PM, Till Mossakowski wrote:
>>>> Am 02.01.2018 um 16:00 schrieb rick:
>>>>> The DOL authors claim to "handle" sequence markers in HETS using "second
>>>>> order logic" which by conformance with MOF and fUML is outside the scope
>>>>> of DOL.
>>>> second-order logic is not outside the scope of DOL.
>>> I have reviewed the RFP and proposal a few times. I understand scope is
>>> defined 6.1 and 6.5.4 and conformance in 6.5.5 of the RFP.
>>>
>>> 6.5.5 establishes conformance of languages and translations of which
>>> none listed are second order logic. Also Annexes D-H do not include a
>>> conformance statement for second order logic.
>>>
>>> How do you justify your claim that second order logic is not outside the
>>> scope of DOL?
>> see section 2.2 "Conformance of an OMS Language/a Logic with DOL" of the
>> DOL standard at http://www.omg.org/spec/DOL/ :
>>
>> "The logical language aspect of an OMS language is conforming with DOL
>> if each logic corresponding to a profile (including
>> the logic corresponding to the whole logical language aspect) is
>> presented as an institution in the sense of Definition 2
>> in clause 10 , and there is a mapping from the abstract syntax of the
>> OMS language to signatures and sentences of the
>> institution."
>>
>> For some specific logics, appendices of the DOL standard establish such
>> a conformance, but of course the scope of DOL is not limited to these.
>>
>>> As an aside, I have searched the for a System F comorphism. Would you be
>>> able to provide a pointer to a paper?
>>>
>> I am not aware of institution-theoretic work on system F.
>>
>> Best, Till
>>
>>
>> _________________________________________________________________
>> To Post: mailto:ontoiop-forum at ovgu.de
>> Message Archives: https://listserv.ovgu.de//pipermail/ontoiop-forum
>> Config/Unsubscribe: https://listserv.ovgu.de/mailman/listinfo/ontoiop-forum
>> Community Files (open): http://interop.cim3.net/file/pub/OntoIOp/
>> Community Wiki: http://ontoiop.org
>>
>>
> _________________________________________________________________
> To Post: mailto:ontoiop-forum at ovgu.de
> Message Archives: https://listserv.ovgu.de//pipermail/ontoiop-forum
> Config/Unsubscribe: https://listserv.ovgu.de/mailman/listinfo/ontoiop-forum
> Community Files (open): http://interop.cim3.net/file/pub/OntoIOp/
> Community Wiki: http://ontoiop.org