HoTT, modal Logic, semantic web, and Scala

[Henry Story]

Hi all,

   just a quick introduction to help you understand how I got here, which

will also help understand the questions that follows:

    I studied  analytic philosophy as an undergraduate and postgraduate 

in London, and my favorite philosopher was David Lewis [0]. Then running 

out of money I remembered I could program, and ended up working at 

AltaVista  (1995-2001) the famous search engine. From 2004 I worked at 

Sun Microsystems on the semantic web and linked data (2004-2010) which 

brought me back to philosophy ( Tim Berners Lee famously quipped that the web is now 

philosophical engineering). Since then I have been working in Scala developing a semantic

web library [1]. Scala of course soon enough brought me to Category theory ( e.g. scalaz 

libraries [2] ), and I have been reading some category theory introductory books since

April. At the recent Scala eXchange conference in London [3] I talked shortly to 

Odersky the author of Scala and he mentioned that there was an even more 

foundational mathematics called HoTT. I was surprised, as it is not every day that 

one discovers that something is happening here. So  of course I had  to look :-) 

  I have read the first 80 pages of the HoTT book with relative ease over X-mass.

I can see it is getting a bit more difficult. But it has already helped me see a) the

very close similarity to Scala 2) how proofs and type systems relate and why 

very advanced Scala developers keep arguing that way.

  So what I am interested is to see how I can start mapping my intuitions from 

David Lewis and the semantic web to HoTT and vice versa. The modal logic part

is short and in chapter 7, so it's going to take me some time to get there.

In David Lewis' philosophy of Language a proposition is identified with a set of

possible worlds: those in which the proposition is true. For a proposition to be

true is for the actual world to be an element of that set [4]. This intuition was taken

on by the semantic web [5], and I think helps explain the open world assumption

that underlies it. David Lewis does allow for different levels of granularity of meaning

which take grammar into account, as else all mathematical truths would have the

same meaning: the set of all possible worlds.

  In HoTT a proposition is identified with a type, which is pretty close to a set. And

also HoTT allows proofs ( arguments ) to be taken into account, so that

one has a feeling that that could be a different way to deal with necessary truths.

The link to the semantic web could be made via Benjamin Braatz category theory 

based thesis 

 "Formal Modelling and Application of Graph Transformations in the Resource

 Description Framework" [6] 

Possible worlds can also be thought of higher dimensional spaces [7], so

perhaps that is a way to link these to Topology and so to HoTT?

It is also intriguing that David Lewis' last book before his death was on 

Mereology where he reduces ( tries to? I can't tell) set theory to the 

part/whole relation where paths between objects make their appearance.

The part that would need investigation and that is not in the HoTT book

are Counterfactuals, such as "If Kangaroos had no tails they would

topple over" which David Lewis analyses as the closest possible worlds

in which kangaroos have no tails are those in which they topple over. This

requires a relation of similarity between worlds, and so goes beyond the

simple modal logics described in chapter 7 of HoTT ( which I only partially 

understand having only reached p 75 of the book.

I have been very intrigued by the relation of modalities to monads, as I 

have had the feeling they were related for a while. So I am happy to see

that they are indeed related as explained in the notes of chapter 7. Hopefully 

I can get to the point where I understand that better soon.

I hope these pointers may be of interest to members of this group. Perhaps

as a result someone here can help me align my intuitions here. 

All the best for the new year,

  Henry Story

[0] see his papers here:

     http://www.andrewmbailey.com/dkl/

   and perhaps most interestingly of all his book Counterfactuals and his thesis Convention

[1] https://github.com/w3c/banana-rdf

[2] https://github.com/scalaz/scalaz

[3] you will find a list of talks on lambda calculus, inferencing in the type system, and my

talk on building a distributed secure social web  ( you need to log in to see these talks )

   https://skillsmatter.com/conferences/1948-scala-exchange-2014#skillscasts

[4] See the first paragraph of David Lewis' Language and Languages

   http://www.andrewmbailey.com/dkl/Languages_Language.pdf

[5] see the short section on possible worlds in the RDF 1.0 Semantics specification

    http://www.w3.org/TR/2004/REC-rdf-mt-20040210/

    ( I think this has been removed from that document by later less bold thinkers )

[6] https://www.researchgate.net/publication/40635984_Formal_Modelling_and_Application_of_Graph_Transformations_in_the_Resource_Description_Framework

[7]  https://www.youtube.com/watch?v=gg85IH3vghA

[Jon Sterling]

Hi,

 

Just a few notes:

 

1. Scala's relation to HoTT is best cast as a relationship with type theory in general, not homotopy type theory (i.e. homotopy is an interesting interpretation of type theory which is not more or less similar to Scala than type theory).

 

2. Can you point to where in [7] there is an analogy between higher dimensional spaces and possible worlds semantics? (The video's a bit long)

 

3. Worlds are an interesting place to look in type theory, though I am not sure whether HoTT has anything new to say there. Modal type theory is also very interesting, and there has been some work in HoTT considering new kinds of modalities.

 

Kind regards,

Jon

--

You received this message because you are subscribed to the Google Groups "HoTT Amateurs" group.

To unsubscribe from this group and stop receiving emails from it, send an email to hott-amateur...@googlegroups.com.

For more options, visit https://groups.google.com/d/optout.

 

[Julian Michael]

Hi Henry,

Thank you for sharing your interesting story. I'm also a logic/semantics/Scala guy (and a HoTT amateur). I have some input about your suggestions. I'm not an expert on type theory so (someone who knows better) please correct me if I draw any erroneous connections.

In David Lewis' philosophy of Language a proposition is identified with a set of

possible worlds: those in which the proposition is true. For a proposition to be

true is for the actual world to be an element of that set [4]. This intuition was taken

on by the semantic web [5], and I think helps explain the open world assumption

that underlies it. David Lewis does allow for different levels of granularity of meaning

which take grammar into account, as else all mathematical truths would have the

same meaning: the set of all possible worlds.

Not just with HoTT, but with type theory generally, the semantics get a lot more complicated than just "a set of possible worlds." A simple type theory corresponds to intuitionistic, rather than classical, propositional logic, and a dependent type theory has something more like an intuitionistic first-order logic embedded in it. In that sense, at least simple type theory already has a "modal logic" because it can be described in terms of Kripke frames. Before making sense of any of these connections you're drawing, you'd need to determine how to correspond types (or just propositions in HoTT) to sets of possible worlds.

 

  In HoTT a proposition is identified with a type, which is pretty close to a set. And

also HoTT allows proofs ( arguments ) to be taken into account, so that

one has a feeling that that could be a different way to deal with necessary truths.

I'd be careful making this connection. Using a proof within a larger one—which you might then "abstract out"—is just lambda abstraction, which corresponds to implication. It'd be rather ambitious to say a modality like "necessarily" already exists in HoTT and is waiting to be discovered, because I'm fairly sure there are people who disagree on what "necessarily" should mean.

  

The part that would need investigation and that is not in the HoTT book

are Counterfactuals, such as "If Kangaroos had no tails they would

topple over" which David Lewis analyses as the closest possible worlds

in which kangaroos have no tails are those in which they topple over. This

requires a relation of similarity between worlds, and so goes beyond the

simple modal logics described in chapter 7 of HoTT ( which I only partially 

understand having only reached p 75 of the book.

This is just one interpretation of counterfactuals. Another one (which I will blindly hazard is more common, at least in AI research) is based on Judea Pearl's notion of causality. There are plenty of features of natural language expression that aren't obvious in HoTT, for example, intensional meaning (which you hinted at earlier) might have to with the structure and equivalence of types, selectional restrictions might have to do with dependent products, copular sentences might have to do with subtyping... etc. There's plenty of work to be done.

If you're interested in connections between HoTT and natural language semantics (this is a topic of interest to me too), then you might want to look at the work of Nissim Francez on proof-theoretic natural language semantics and Zhaohui Luo's work on NL semantics with dependent type theory. So far I haven't been able to find any work bringing the insights of HoTT into the picture (though this might change soon if I have anything to do with it).

I hope my comments are helpful to you.

Regards,

Julian

[Henry Story]

> On 2 Jan 2015, at 19:45, Jon Sterling <j...@jonmsterling.com> wrote:
>
> Hi,
>
> Just a few notes:
>
> 1. Scala’s
> relation to HoTT is best cast as a relationship with type theory in general, not homotopy type theory (i.e. homotopy is an interesting interpretation of type theory which is not more or less similar to Scala than type theory).

Ah yes, that’s probably also why the first chapter of the HoTT book is so easy to read
for a Scala developer. The notation is nearly the same ( except that scala adds an OO
part to it ). It took me some time to understand quantifications as Domains of functions, but
it works well once understood.

Also the explanation of dependent types is very useful in understanding
libraries such as shapeless that make very heavy use of them

https://github.com/milessabin/shapeless
http://www.infoq.com/interviews/sabin-types

>
> 2. Can you point to where in [7] there is an analogy between higher dimensional spaces and possible worlds semantics? (The video's a bit long)

The first ten minutes of the video make it quite clear. ( I only discovered the
full hour video recently ).
I wrote up a short summary of the 10 dimensions on a blog a while ago
https://blogs.oracle.com/bblfish/entry/the_10_dimensions_of_reality

This presentation is very simple and intuitive. I am not sure if it
correct, people here will be better apt at saying, but it helps
guide intuitions.

If you read David Lewis carefully he starts with a world which we would
call a universe, adds a distance relation, and then through various arguments
looks at smaller and smaller distances between worlds, until it becomes a
continuum. So that David Lewis' modal logic to a higher dimensional
interpretation is left open.

This in fact brings up the question as to the relation of modal logic and
string theory. It is very odd that Stephen Hawkins does not seem to mention
modal logic, even though he defends a multiverse idea of string theory.
Or at least I could not find any reference on the internet to a discussion
between these two thinkers.

The recent issue of Wired has a long sectionon Hawkins. It does not say
much that is very meaty on the subject, but I did quote Kip Horne,
professor of theoretical physics at Caltech

"As he [ Hawkins] lost his hands and could no longer write
equations, he developed, far better than anyone else has in
history, an ability to use geometrical and topological
images in his head to solve problems. That enabled him to
see things that other people didn't see. It was central to
a lot of his discoveries"

So if you put this together with HoTT using Topology as a
interpretation ( semantics ? ) of type theory one has to wonder
if the aim of hott is to help other mathematicians become more
intuitive about their reasoning....

Of course this also makes me wonder if there is a relation
between the strings of string theory and the notion of fibrations
used in HoTT. ( that's very likely a dumb question but I have
very little knowledge of topology )

>
> 3. Worlds are an interesting place to look in type theory, though I am not sure whether HoTT has anything new to say there. Modal type theory is also very interesting, and there has been some work in HoTT considering new kinds of modalities.

yes, I think there must be something worth researching there.

Social Web Architect
http://bblfish.net/

[Michael Shulman]

The possible-worlds interpretation of modal logic has, of course,
received a lot of study by modal logicians and philosophers in
addition to Lewis:
http://plato.stanford.edu/entries/logic-modal/
http://plato.stanford.edu/entries/possible-worlds/

From a mathematical standpoint, this perspective amounts to a
construction of (co)monads representing modal operators as composites
of base change functors. A simple example of how this works is
described at
http://ncatlab.org/nlab/show/necessity+and+possibility
More complicated systems of worlds require more complicated
constructions, but the basic ideas are similar. The "worlds at which
a proposition is true" are incorporated as its meaning in the
semantics, but not *internally* to the model (as the elements of a
type) but rather externally.

Classical modal logic acts only on propositions, but in dependent type
theory we can consider in addition modalities that act on
non-proposition types. The modalities which arise naturally in HoTT,
such as truncation and the cohesive modalities, do act on all types
(not just propositions). However, it's a bit of a stretch to think of
those modalities as having much to do with the classical modalities
"necessity" or "possibility".

David Corfield has been thinking a lot about the relation of HoTT to
philosophy, and particularly the treatment of modalities and what it
would mean to extend the classical modalities to non-proposition
types. We've had some interesting discussions at the n-Category Cafe
and the n-Forum, e.g.
https://golem.ph.utexas.edu/category/2013/04/modal_types.html

Hope this helps!
Mike

[Hendrik Boom]

On Fri, Jan 02, 2015 at 09:10:41PM +0000, Henry Story wrote:

Highly speculative stuff coming.

There's a new take on topology. Instead of focussing primarily on
open sets, possibly defined by a distace measure, the constructive
approach starts with a relation of distinguishability. Classically,
two, say, real numbers are either the same or different, but the
failure of the law of the excluded middle provides the constructivist
with a more nuanced distinction. This, properly handled, leads to a
topology. nowadays called the "Natural topology".

You can get the idea from the first parts of Frank Waalldijk's book,
http://www.fwaaldijk.nl/natural-topology.pdf

>
> This in fact brings up the question as to the relation of modal logic and
> string theory. It is very odd that Stephen Hawkins does not seem to mention
> modal logic, even though he defends a multiverse idea of string theory.
> Or at least I could not find any reference on the internet to a discussion
> between these two thinkers.

There's an interesting series of papers on 'daseinisation'. I'd start
with The physical interpretation of daseinisation. Or any of thepapers
you find while googling 'daseinisation' It appears to be an attempt to
describe an umderlying reality for QM that we only get glimpses of
from our 'classical perspectives', which express our limited ability
to observe.

It makes heavy use of topos theory. Which may be able to expressed
using type theory, which is a kind of internal logic for toposes.

I admit I haven't made enough sense of this daseinisation stuff to
really recommend it, but it looks promising.

>
> The recent issue of Wired has a long sectionon Hawkins. It does not say
> much that is very meaty on the subject, but I did quote Kip Horne,
> professor of theoretical physics at Caltech
>
> "As he [ Hawkins] lost his hands and could no longer write
> equations, he developed, far better than anyone else has in
> history, an ability to use geometrical and topological
> images in his head to solve problems. That enabled him to
> see things that other people didn't see. It was central to
> a lot of his discoveries"

Michio Kaku says something similar about himself, when he was obsessing
over soe QM problems while undergoing militaty basic training and had
no access to paper and penncil whilt belly-crawling under a field of
machine-gun fire. He learned to visualise, and to keep equations
simple and symmetrical.

> So if you put this together with HoTT using Topology as a
> interpretation ( semantics ? ) of type theory one has to wonder
> if the aim of hott is to help other mathematicians become more
> intuitive about their reasoning....
>
> Of course this also makes me wonder if there is a relation
> between the strings of string theory and the notion of fibrations
> used in HoTT. ( that's very likely a dumb question but I have
> very little knowledge of topology )

I've heard that topological reasoning has been used in some of the
attacks on some difficult QM problems. It makes me wonder, too.

And, of course, there's also loop quantum gravity. I have no idea
whether that fits in. These are all different attacks on the difficult
problem of quantising the gravitational field. To the extent that
they're right, there mist be some relationship bwtween them. Just like
Dirac unified wave mechanics and matrix machanics by discovering they
resulted from different kinds of coordinate systems on
infinite-dimensional spaces.

-- hendrik

[Henry Story]

Thanks for the great pointers Julian. I can see that replying to e-mails on this

list is no small task. It can potentially take a year of reading in some cases :-)

On 2 Jan 2015, at 19:45, Julian Michael <julianjo...@gmail.com> wrote:

Hi Henry,

Thank you for sharing your interesting story. I'm also a logic/semantics/Scala guy (and a HoTT amateur). I have some input about your suggestions. I’m not an expert on type theory so (someone who knows better) please correct me if I draw any erroneous connections.

In David Lewis' philosophy of Language a proposition is identified with a set of

possible worlds: those in which the proposition is true. For a proposition to be

true is for the actual world to be an element of that set [4]. This intuition was taken

on by the semantic web [5], and I think helps explain the open world assumption

that underlies it. David Lewis does allow for different levels of granularity of meaning

which take grammar into account, as else all mathematical truths would have the

same meaning: the set of all possible worlds.

Not just with HoTT, but with type theory generally, the semantics get a lot more complicated than just "a set of possible worlds." A simple type theory corresponds to intuitionistic, rather than classical, propositional logic, and a dependent type theory has something more like an intuitionistic first-order logic embedded in it. In that sense, at least simple type theory already has a "modal logic" because it can be described in terms of Kripke frames. Before making sense of any of these connections you're drawing, you'd need to determine how to correspond types (or just propositions in HoTT) to sets of possible worlds.

 

  In HoTT a proposition is identified with a type, which is pretty close to a set. And

also HoTT allows proofs ( arguments ) to be taken into account, so that

one has a feeling that that could be a different way to deal with necessary truths.

I'd be careful making this connection. Using a proof within a larger one—which you might then "abstract out"—is just lambda abstraction, which corresponds to implication. It'd be rather ambitious to say a modality like "necessarily" already exists in HoTT and is waiting to be discovered, because I'm fairly sure there are people who disagree on what "necessarily" should mean.

  

The part that would need investigation and that is not in the HoTT book

are Counterfactuals, such as "If Kangaroos had no tails they would

topple over" which David Lewis analyses as the closest possible worlds

in which kangaroos have no tails are those in which they topple over. This

requires a relation of similarity between worlds, and so goes beyond the

simple modal logics described in chapter 7 of HoTT ( which I only partially 

understand having only reached p 75 of the book.

This is just one interpretation of counterfactuals. Another one (which I will blindly hazard is more common, at least in AI research) is based on Judea Pearl’s notion of causality.

Thanks very much for this pointer. 

I watched a few of his presentations to get a bit of an idea

of his thesis. http://bayes.cs.ucla.edu/BOOK-2K/ . Very interesting stuff.

The relation between causality and counterfactuals has been very close since 

David Lewis’ initial paper on it. A book collecting a set of articles on the topic

summarising the research edited by John Collins, Ned Hall and L.A. Paul

came out in 2004 called « Causation and Counterfactuals ». (It’ s a pitty that

Judea Pearl was not part of the authors.) And indeed  which of causation or

counterfactuals is primary is an interesting question: I suppose they are equivalent 

if one is correctly defined in terms of the other: in that case you can inverse

the direction of explanation.

Judea Pearl has a lot of references to David Lewis in his book and in his

talks. His breathrough is to make this calculable ( dropping methaphysics) 

so that it can work « for a dumb computer » given a model, which is of 

course really interesting for me as  a programmer :-)

My guess is that the metaphysical and the computational

meet at infinity, meaning that the metaphysical view is an idealisation 

over all  inferences on all facts. It allows us to speak of what

would have happened had caesar not crossed the rubicon, ( a lot would 

certainly have been very different ), even if we can’t really say much 

about it. As an idealisation of infinite sets of coherent sentences,  

David Lewis always gives two versions of his model of counterfactuals 

one in terms of infinite sets of coherent sentences, and one in terms of

real but non actual existing worlds - there are some operations allowed in

one but not in the other interpretation ). At the same time a computational

version of the problem is of course really helpful. :-)

This is similar to Robert Brandom’s work which was mentioned on this 

list some time ago (he was also a student of David Lewis - his beard and his 

development of score keeping in a language game in « Making it explicit » 

are two clear give aways there ) who moves from metaphysics to 

inferentialism. So there is a pattern here.

 

There are plenty of features of natural language expression that aren't obvious in HoTT, for example, intensional meaning (which you hinted at earlier) might have to with the structure and equivalence of types, selectional restrictions might have to do with dependent products, copular sentences might have to do with subtyping... etc. There's plenty of work to be done.

If you're interested in connections between HoTT and natural language semantics (this is a topic of interest to me too), then you might want to look at the work of Nissim Francez on proof-theoretic natural language semantics and Zhaohui Luo's work on NL semantics with dependent type theory. So far I haven’t been able to find any work bringing the insights of HoTT into the picture (though this might change soon if I have anything to do with it).

I look forward to the results of your research, as I won’ t have much time to follow this in detail.

Zhaohui Lui’s statement on his page

"To solve this problem, we have conducted a preliminary study [3]. It shows that a theory of subtyping is not only useful but crucial in giving a natural and adequate type-theoretical semantics and that coercive subtyping [4] provides us with such a framework. The first goal of the current project is to develop this type-theoretical approach, employing modern type theory with coercive subtyping to obtain an adequate formal account of lexical semantics as studied by Pustejovsky [6], Asher [1] and others. »

So does this mean that Scala’s mixing of type theory with OO notions of

subtyping is on the right path?

I hope my comments are helpful to you.

yes. I am moving up the exponential green curve below very fast :-)

Regards,

Julian

[Julian Michael]

Henry,

Thanks for the comments. I should definitely look more into Lewis and Brandom—I haven't read their work.

To address your last question, Luo's approach of coercive subtyping is completely different from Scala's subtyping, which is either nominal (i.e., based on inheritance) or structural (i.e., like subsumption-based subtyping, treating objects as records)—although Scala does allow implicit conversions, which you can kind of use in the same way. Also, Scala does have a tiny bit of dependent typing ("path-dependent types") but this is nowhere near the expressivity of a Martin Löf style system. So I wouldn't relate Luo's approach to Scala. Scala's type system was designed for programming, not formal mathematics or natural language semantics.

<knowledge.jpg>

Regards,

Julian

[Urs Schreiber]

Interesting discussion. Here are some comments.

It is refreshing to see the question why Hawking (note the spelling)
does not consider modal logic. You are in for some surprises about how
utterly fragmented the modern academic world is.

One place where the relation between physicist's "multiverse" and
modal logician's "many worlds" is at least mentioned is on the nLab
here

http://ncatlab.org/nlab/show/multiverse#RelatedConcepts

Notice also the references on physicist's multiverse there. Anyone who
is going to be serious about relations to physics and maybe even
string theory will at some point have to realize that the set of
physics authors that feature prominently in standard book stores is
fairly disjoint from those authors who write the relevant research
articles. Better check out some book from this list here

http://ncatlab.org/nlab/show/books+and+reviews+in+mathematical+physics

Regarding the possible relation of HoTT to physics and maybe to string
theory: As usual, I am uninhibited about the following shameless plug,
since it is as relevant to the question as it is shameless:

adding to HoTT a suitable adjoint triple of modal operators turns it
into "cohesive HoTT"

ncatlab.org/nlab/show/cohesive+homotopy+type+theory

and a remarkable fact is that cohesive HoTT by itself knows a great
deal about modern gauge field theory and structures appearing in
string theory. This article here with Mike Shulman
http://ncatlab.org/schreiber/show/Quantum+gauge+field+theory+in+Cohesive+homotopy+type+theory

indicates the nature of cohesive HoTT and gives a very brief outlook
on what it has to say about physics, while this text here

http://ncatlab.org/schreiber/show/differential+cohomology+in+a+cohesive+topos

means to eventually give a comprehensive account of the relation to
physics. Related introductory talk notes include for instance these
here

http://ncatlab.org/schreiber/show/Synthetic+Quantum+Field+Theory

Anyone serious about understanding how this works might want to start
with the following text which gives an introduction to classical field
theory formulated all in terms of cohesion and in a way that lends
itself to formalization in cohesive HoTT

http://ncatlab.org/schreiber/show/Classical+field+theory+via+Cohesive+homotopy+types

[Henry Story]

Thanks Urs for the links below. Your book
"Differential cohomology in a cohesive 1-topos"
is pretty amazing. I skimmed through the 800 pages
and I think I'd might be able to read at least the
first two chapters over time. The overview it gives of
how science, topology and homotopy type theory fit
together has helped me understand to a much greater
extent the attraction of category theory. So I have
been reading some introductory course on topology [1],
and am trying to get to the point where I understand
the Grothendieck Topos [2]. At least here I can see how
these build up on each other, and what I need to
learn. Hopefully I'll be able to then use these
concepts with Scalaz, so that I get to the point where
I can have an intuitive feel about them.

But the holidays are over and I need to get back to the
building a distributed social web using the semantic
web as a priority :-)

Here modal logic pops up very quickly in terms of belief
contexts. Every graph I download on the web I can put into
my local graph store related to the name of the URL at
which I picked it up. This graph expresses a restriction on
a set of possibilities expressed by some agent. Say a friend
writes down his profile in RDF and then links to his friends
profiles on their own server. I can follow those links
to those graphs, and merge the relations to see what the world
would look like if all the graphs were true. If I don't like
it I can remove a graph from the union, perhaps patch a remote
resource using HTTP Patch as explained in the LDP
specifications [3]

Writing the category of Graphs, and graph stores is easy in
Scala and should be easy in HoTT, since Benjamin Braatz gave
a definition for it in Category Theory [4] . If I do then I'll
have a bunch of new types Node, URI, Triple, Graph, Store [5].
So if I write these types out in HoTT I'd end up with statements
like the following

timblProfile: Graph

if I have a type of PointedGraph I can construct one for Tim Berners Lee

timbl ≣ (URI("http://www.w3.org/People/Berners-Lee/card#i"), timblProfile) : PointedGraph

So everything is typed in what I wrote above. But we end up with
graphs containing relations that are flexibly typed - because of the
open world assumption of RDF: we don't always know the types of
all the objects related to by the relations expressed there.

If I construct a graph store I may be able to create RDF relations relating
an agent to a graph, by the relation of say dox:noTrust or
dox:believe etc, in which case I'd have a store stating that someone
does not believe what someone else says, even if by following links I
find someone else who does believe it. This is not inconsistent:
it is a basic feature of intellectual life that one can deal with
people who disagree with one. These are the modal contexts of belief
that I must use as soon as I work on the web.

So I suppose the question is what is the relation between RDF and
HoTT, given that one has a category of RDF as Benjamin Braatz describes
it. Perhaps that will help give some hints as to the other modal
questions that arose in this very rich discussion.

Henry


[1] https://www.youtube.com/playlist?list=PLF94A6F65866F3F31
[2] Olivia Caramello interview in France on the subject
https://www.youtube.com/watch?v=sM_9R63qU6o
[3] http://www.w3.org/2012/ldp/wiki/Main_Page
[4] "Formal Modelling and Application of Graph Transformations in the Resource Description Framework"
https://www.researchgate.net/publication/40635984_Formal_Modelling_and_Application_of_Graph_Transformations_in_the_Resource_Description_Framework
( should a reference on this be on the NLab wiki ? )
[5] These are expresses as path dependent types in banana-rdf in Scala here
https://github.com/w3c/banana-rdf/blob/master/rdf/common/src/main/scala/org/w3/banana/RDF.scala
See the video for more details
https://skillsmatter.com/conferences/1948-scala-exchange-2014#skillscasts

[Alan Jeffrey]

Peter Patel-Schneider and I wrote a categorical treatment of RDF in:

Integrity Constraints for Linked Data.
Proc. Int. Workshop Description Logics. 2011.
http://ect.bell-labs.com/who/ajeffrey/papers/dl11.pdf

The summary is that you can build a symmetric monoidal category of graph
stores. There's no connection with HOTT, except that there's a
formalization in Agda,

Alan.

[Henry Story]

> On 7 Jan 2015, at 15:28, Alan Jeffrey <ajef...@bell-labs.com> wrote:
>
> Peter Patel-Schneider and I wrote a categorical treatment of RDF in:
>
> Integrity Constraints for Linked Data.
> Proc. Int. Workshop Description Logics. 2011.
> http://ect.bell-labs.com/who/ajeffrey/papers/dl11.pdf
>
> The summary is that you can build a symmetric monoidal category of graph stores. There's no connection with HOTT, except that there's a formalization in Agda,

Thanks for the link Alan, which brings up some interesting
parallels with HoTT.

As a way of introduction to RDF let me start by noticing that
in the HoTT book the signs f, P, Q, etc... are used to mean many
different things. For example on page 23 f is the function
of addition

f(x) :≡ λy. x + y

but on page 26 it is

f : ∏(a: A)∏(y: B(x)) C(x,y)

and this is all over the book :-) Of course the human reader has
no trouble working out the context. But if one looks carefully
at books on logic, the interpretation of a sign is meant to be
universal! So one could say that this is the problem solved by
RDF: it simply decides to use URIs (Universal Resource Identifiers )
as symbols. These have the advantage of allowing a globally distributed
name creation to be able to take place, without fear of name clashes.
Add to that the Linked Data principle of restricting oneself to URLs
and to place the definition of a term at the location of the URL
and one gets an automatic way of linking information together in
a distributed information space.

Of course URLs are tedious to write, and so would not appeal to a
mathematician, but that is why it is an engineering project: the
machines do that parsing and reasoning for us. There are syntaxes
that make it easier to type out such as Turtle or the more powerful
N3 [1].

So a fun exercise for the HoTT amateurs is: what would HoTT look
like if you were to use URIs as symbols? What consequences would
it have if one were to think of HoTT definitions linked to each
other across the web?

This can lead us back to Alan's paper. There is a parallel with HoTT and
OWL (Ontology Web Language) [2] in so far as OWL tends to makes a
stronger distinction between objects and types than the base RDF
infrastructure necessitates. The TBox statements are statements
about types, and they describe what consequences follow from the
use of a term. Such a definition can only set some constraints on
the use of a term it is true, since many other consequences as Robert
Brandom would point out are part of the meaning of a term: e.g.
one could say that every human has two parents recursively, but one
risks denying evolution in doing so. Still as with HoTT that way of thinking
moves reasoning to the type system - a worthwile parallel to note. How far
can one take this parallel? What are the differences?

One could add to this that relations in RDF are not that far from
paths between objects ( arrows ? ) except that the paths are named,
so that one can have a set of different named paths between two objects.

eg a foaf:knows b .
a o:parent b .

In which case the identity relation owl:sameAs is very much like the
a = b type in HoTT. This is even more clear if one uses the N3 graph
quotation notation to distinguish statements and statements about
statements by using { ... } .

One could then write

{ a owl:sameAs b } <=> { b owl:sameAs a }

as a path between paths.

If one ties OWL to linked data as Alan paper starts to do, then one
should also put the OWL definitions of the term at the URL of the
document describing the term [3]. Factual statement and ontological
statements can thus be discovered using exactly the same linked data
principles.

Once one sees this parallel I have the feeling that the Alan's paper
can be nicely simplified. Could one not redescribe what is going on in
terms simply of graphs, union of graphs (as defined by the RDF specification )
and reasoning over graphs? Ie, in terms of modalities?
The examples in that paper can thus be rewritten as

@prefix foaf: <http://xmlns.com/foaf/0.1/> .
@prefix bob: <http://bob.example/#> .
@prefix alice: <http://alice.example/#> .

G1 = { bob: foaf:primaryTopic bob:me .
bob:me foaf:knows [ foaf:homepage alice: ] . }

G2 = { alice: foaf:primaryTopic alice:me . }

foaf = { ...the set of foaf statements... }

Reasoning can then just be done over the unions over the graphs
( assuming one has first normalised all blank nodes ) with the
following

{ G1 U G2 U foaf } owl:reasoning _:InferentiallyCompletedGraph .

where owl:reasoning is a relation I made up to relate a graph
to a graph which would be the completed reasoning using owl rules
over the initial graph. ( I suppose it would be the empty set {}
in case of a contradiction? )

If that is correct then one could verify if this still does form
a symmetrical monoidal category. If a monoidal category is not related
to monads or to modal thinking then I doubt it. Because there is no
necessity to follow all links and to merge all data. In so far as a
graph uses a term defined in another graph there is the presumption
that one should work with the merged information, but that does not
always hold. For example when dealing with security as we do with
WebID TLS [4], where one must start with a skeptical attitude,
such an full inclusion of linkes would allow an enemy to determine
your access control rules. That is why the modal/methapysical ( let us
say idealised ) logic of David Lewis is helpful. The meaning/(interpretation?)
of a graph are all the set of possible ways the world could be that
are compatible with that statement. Less metaphusically, more computationally
and so more in Brandom's style, its all the other possible ways you can union a graph
with other statements without contradiction. Merging two graphs just tells me what
the world would look like if both were true ( or what I would be committed to if
I committed to both) but it does not tell me that they are true, or that I should
commit myself thusly. That is up to the human agent to determine based
on his intuitions, context, etc...


So OWL it has always seemed to me is a way of doing reasoning without
or with minimal modality ( and that is an both a limitation and a strenght).
That is if one were to translate OWL into logic it would only require purely
material conditionals. If you believe X then owl tells you what else
you should believe. But it is clearly not designed for doxastic
modal statements, which requires the quotation of graphs, and what
is known in philosophy as the opaqueness of belief contexts. The well
know example is

Lois Lane believes superman is great

But she would not agree that Clark Kent is great, even though
both have the same referent. Here belief is a relation to a
propositional attitude, which in the semantic web could reasonably
be modelled as a relation between a person and a graph where the
belief context can be opaque. This would then also allow dissagreement
between beliefs to be expressed, using as basis the rel=nofollow link
pushed by Google in the blogging space [5].

Anyway these are questions that I keep wondering about when programming
in Scala and working with the semantic web. But the Scala mailing list is
not the best place to conduct such a discussion. Hopefully this is not too
far out of scope for this mailing list, and has prooved interesting
to other subscribers.

All the answers I have received until now here have been extreemly
helpful :-)

Henry


[1] http://www.w3.org/TeamSubmission/n3/
[2] http://www.w3.org/TR/owl2-overview/
[3] making sure not to confuse the URL of the
document and the URL of the term by having the
term be a #url as explained in say the WebID
document
http://www.w3.org/2005/Incubator/webid/spec/identity/
[4] http://www.w3.org/2005/Incubator/webid/spec/
[5] http://en.wikipedia.org/wiki/Nofollow

>
> Alan.
>
> On 01/06/2015 07:05 PM, Henry Story wrote:

>> [snip some of the thread not related to this theme]

>>> [snip discussion about HoTT and physics]

[Andrej Bauer]

On Thu, Jan 8, 2015 at 3:48 PM, Henry Story <henry...@gmail.com> wrote:
> So a fun exercise for the HoTT amateurs is: what would HoTT look
> like if you were to use URIs as symbols?

Let us not mix up everything here. The exercise you suggest sound
neither fun nor useful. There is nothing mysterious about the fact
that symbol 'f' gets used for one thing in one place and another in
another place. We are using local scoping, which is commonplace in
mathematics and programming, contrary to your claim that logic books
prescribe a different standard. *Certain* logic books speak of
first-order languages which use "global" symbols, but those would be
logic books of a very classical nature with specific goals in mind. In
type theory and programming languages the notion of a scope of a
symbol is very well understood and several techniques are known for
dealing with the local nature of scoping (and they do not include
passage to global identifiers).

So these issues sound to me as being just about formalism and syntax
andt hey have nothing to do with the content of HoTT itself.

> What consequences would
> it have if one were to think of HoTT definitions linked to each
> other across the web?

Again, this is a matter of form and technique, not of the content of
HoTT, but since you ask, here it is:
http://hott.github.io/HoTT/coqdoc-html/

With kind regards,

Andrej

[Henry Story]

> On 8 Jan 2015, at 17:30, Andrej Bauer <andrej...@andrej.com> wrote:
>
> On Thu, Jan 8, 2015 at 3:48 PM, Henry Story <henry...@gmail.com> wrote:
>> So a fun exercise for the HoTT amateurs is: what would HoTT look
>> like if you were to use URIs as symbols?
>
> Let us not mix up everything here. The exercise you suggest sound
> neither fun nor useful. There is nothing mysterious about the fact
> that symbol 'f' gets used for one thing in one place and another in
> another place. We are using local scoping, which is commonplace in
> mathematics and programming, contrary to your claim that logic books
> prescribe a different standard. *Certain* logic books speak of
> first-order languages which use "global" symbols, but those would be
> logic books of a very classical nature with specific goals in mind. In
> type theory and programming languages the notion of a scope of a
> symbol is very well understood and several techniques are known for
> dealing with the local nature of scoping (and they do not include
> passage to global identifiers).
>
> So these issues sound to me as being just about formalism and syntax
> andt hey have nothing to do with the content of HoTT itself.

Yes, I program in Scala, before that in Java, in Prolog and many
other languages, so you imagine that I am au fait with local
scoping. None of these languages do a very good job of integration
of other information in a global space. They were not designed
to do this and so this is not a critique of them, just as it
is not a critique of HoTT that it be readable and writeable by
Mathematicians. To take Prolog one of the languages closest logic
it's built in closed world assumption is an immediate stumbling block
to doing what the semantic web is attempting to do.

So the thought experiment was a way to try to make understandable
the technical/social breakthrough in RDF, as a way of introduction
to it, and just to work out where the differenes lie - so as to
better be able to understand how the two would tie together.

>
>> What consequences would
>> it have if one were to think of HoTT definitions linked to each
>> other across the web?
>
> Again, this is a matter of form and technique, not of the content of
> HoTT, but since you ask, here it is:
> http://hott.github.io/HoTT/coqdoc-html/

I have not coded in coq, and seeing how it is being used here am quite
interested to learn. ( It would be nice if I could have a coq to
JS compiler, or perhaps even to Scala [1] :-)

Here the definitions seem to all be importing other definitions that
are on the same web server. Can I import definitions that are on another
web site? Can that import further definitions from further web sites
or link to further facts?

I am asking because I can also put Scala code on the web such as here

https://github.com/w3c/banana-rdf/blob/master/rdf/common/src/main/scala/org/w3/banana/PointedGraphs.scala

but a Scala compiler does not point at a piece of code and follow links across
the web fetching code and compiling it as it goes along. ( But that does not
prevent me writing an RDF library in Scala that can do that). For one the naming
of an object does not tell me where I can find an authoritative definition for
that object.

Which is exactly what we do with linked data. My WebID links to 50 people
who may link to further 50 people, etc. One day we may this way have a globally
distributed social web of peopel. It would not make sense to have to download
all the information from everyone to be able to display a person's profile.

The thought experiment of adding URIs to HoTT was just an attempt to teasse out
such differences. For all I know it may work :-) Perhaps could write my RDF like
this in a HoTT style

<#me> : foaf:Person .

But a type is a proposition, and I suppose under a very simple set theoretic
notion of meaning, a proposition is just a set and so is a type, so perhaps that
would fit. But one of the points of HoTT is that as a constructive mathematics
I should be able to build the object. <#me> is not really an object I seem to
build. It is a description of someting out there in the world. ( RDF: Resource
Description Framework ).

Hope that helps,

Henry

>
> With kind regards,
>
> Andrej

[1] as suggested for fun by Alexandre Bertails in a talk at Scala.io
conference recently http://scala.io/talks.html#/#NGJ-113