[ontoiop-forum] DOL finalisation

[rick]

Thanks Till for taking the time to answer my questions.

I remain unconvinced that an institution that's not in the proposal is
in scope.

More important though is whether an institution of "second order logic"
exists. And whether the required mapping from the abstract syntax of OMS
to the signatures and sentences of "second order logic" exists. right?

Just to be sure, when you say "second order logic" you mean Henkin
Semantics, right?

I will enjoy reading the reference on type class polymorphism.

Do you claim the paper contains the institution and the mapping? It
seems not as the paper predates (2004) DOL.

If not, could you please provide a pointer?

I briefly scanned the paper. Looks like a great paper.

--
Rick

On 01/04/2018 05:34 PM, Till Mossakowski wrote:
> 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
> 
> 
> 
> _________________________________________________________________
> 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
>