Dependent Types

Hi,

   We have a use case in WAC where we want to state things like the
following:

> Any agent S can edit the comments (to a blog post) that S has created.

This I get the feeling is going to be difficult to express in OWL, which
I am thinking of using to extend the current WAC ontology.

In WAC+OWL we can write things like

<#rule> 
   :accessTo :ResourcesTaggedOver18
   :agentClass :AgentsOver18
   :mode :Read.

where we can described :ResourcesTaggedOver18 and AgentsOver18 by Description.

But I think the problem with the rule I want to express is that it requires 
what are known as Dependent Types. Every agent gets its own rule.

Mind you, this can be expressed using N3 and OWL with: 

```
{ ?s a foaf:Agent } => {
   [] a :Authorization;
     :accessToClass [ 
        a owl:Restriction;
        owl:onProperty iana:author
        owl:hasValue ?s ];
     :mode :Write;
     :agent ?s 
}
```

This is a pretty obvious use case I think.
So it looks like we would need N3.

I wrote this up in a discussion here:
https://github.com/solid/authorization-panel/discussions/261 


By the way, thinking about dependent types I found this 2020 
article "Dependently Typed Knowledge Graphs”
https://arxiv.org/abs/2003.03785

> Reasoning over knowledge graphs is traditionally built upon a hierarchy of languages in the Semantic Web Stack. Starting from the Resource Description Framework (RDF) for knowledge graphs, more advanced constructs have been introduced through various syntax extensions to add reasoning capabilities to knowledge graphs. In this paper, we show how standardized semantic web technologies (RDF and its query language SPARQL) can be reproduced in a unified manner with dependent type theory. In addition to providing the basic functionalities of knowledge graphs, dependent types add expressiveness in encoding both entities and queries, explainability in answers to queries through witnesses, and compositionality and automation in the construction of witnesses. Using the Coq proof assistant, we demonstrate how to build and query dependently typed knowledge graphs as a proof of concept for future works in this direction.

which I still need to read, but I thought would be of interest to members of this group.

Henry

PS. Dörthe, thanks for your answer on the modal concepts mail.
I will send you an answer as soon as I get a bit of time. I have
a lot of deadlines to meet for my EU project.

https://co-operating.systems
WhatsApp, Signal, Tel: +33 6 38 32 69 84‬ 
Twitter: @bblfish

Received on Friday, 24 September 2021 07:55:12 UTC