Background on Knowledge Graphs and Types

In this post, Knowledge Graph indicates information stored in a graph-aware database, usually including some ontology features.

Quite often the same knowledge store includes description of space, time, and/or quantitative signal data.  Such hybrid capability suggests a fuzzy boundary between a "knowledge graph" and other flavors of information storage.

Meanwhile Type Theory refers to a vital trend in mathematics and logic towards harmony with concepts that are familiar in computer science.

In this post I provide some general background for discussion of fun ideas at the intersection of
Knowledge Graphs with Type Theory, without delving too far into specific technology issues.

Introductory Material on KGs and KBs

  •  Technically minded may start with this open access e-book  (Springer PDF + HTML), sponsored by European Union project LAMBDA (Learning, Applying, Multiplying Big Data Analytics):
  • The boss's boss may appreciate this glossy, broadly accessible presentation (PDF) from Pool Party.biz, aka Semantic Web Company (Vienna) :
  • For more depth in applied ontology thinking, check out MK Bergman's work:
    • AI3 blog - outstanding and longstanding
    • KBPedia curated reference ontology (linked below, under example KBs)
    • Bergman's 2018 book A Knowledge Representation Practionary.
  • Engineers interested in RDFS/OWL modeling perspectives should review 

Example Graphs, Datasets, Schemas, and Ontologies

  • Example open access KBs and schema repositories
  •  Example subject ontologies and vocabs, suitable for KG mapping
    • Focused application fields 
    • Broad conceptual fields 
      • Language:  NLP
        • ConceptNet
        • KG-BERT - 2019 paper by Liang Yao, Chengsheng Mao, Yuan Luo
        • Bridges to everything humans describe with words
      • Geography:  GIS
        • Geography and geospatial vocabularies and ontologies are widespread
        • List of ISO standards in digital geography + geomatics, from ISO/TC 211
        • Open Geospatial Consortium - list of open GIS software standards
        • Bridges to earth, ocean, space sciences
      • Humanities:  CIDOC - cultural artifact description, following ISO 21127:2014
        • CIDOC CRM : Conceptual Reference Model, "a formal ontology intended to facilitate the integration, mediation and interchange of heterogeneous cultural heritage information."
    • Most academic fields have ongoing efforts towards standardization of vocabulary, taxonomy, and ontology.  These efforts are important modern manifestations of library science.  

Implementation Patterns for RDF, Gremlin, and other Property Graphs

Here is a taste of active/recent open source KG technology ingredients and design patterns

 Beyond Ontology:  Formal Specification, Proof, and Verification

The connections from assisted theorem proving (ATP) bridge the worlds of  formal mathematics and
digital knowledge science.  Some well-known bridging toolsets are listed below.  As for me, recently
I have been lurching further into the Lean community.  I find it the easiest proof assistant to dabble
in, thanks to a wealth of educational web content.  I also enjoy reading work in Coq and Agda, and experimenting in Idris.   But to keep this reading list short(-ish), we give the most space below to
Lean, which is a CoIC system (calculus of constructions), as are Coq and Agda.   
Here are promised links about the intersection of type models, proofs, and knowledge graphs:

Type Theory meets Semantic Graphs

You guessed it:  Here we are intersecting knowledge graphs with formal types and proofs.

Typed Graph Knowledge - additional conference proceedings, from 2019-20

    Of course, one always finds/re-discovers more and more conferences and sub-conferences.  
    If you have ideas for more links, or other thoughts to share, feel free to reach out on Twizzler: 
    @Stu_B22 or through my biz-card site at Appstract.com


    Popular posts from this blog

    Streaming analytics in Scala using ZIO and Apache DataSketches (part 1)

    Image
    First let's look at a trivial example of streaming analytics using ZIO Streams 2.0.9 (on Scala 2.13). https://scastie.scala-lang.org/6AHfPh02S6m0k7aN6bkacA When run, this Scastie just averages some random numbers (gaussian) in a single input stream.  That code is in the trait AvgFun . But we also see a trait called ParAvgFun with the code for rather painless parallel  implementation, using ZIO chunks, via ZStream's  grouped , zipWithIndex , and groupByKey .  Across these two traits, the clean reusability of ZSinks in different pipelines shows a nice design win for the ZIO Streams API.   The code in  ParAvgFun.parAvgUsingChunks  demonstrates a terse and reasonably efficient design for accumulating results using parallel ZStreams (within a single process).  It is applicable to  simple cases where the stream elements are lightweight and similar, and the underlying operations are uniformly easy (like summing numbers).  When instead there is great variability in the cost of proces
    Read more

    Overview of AxLam model : Nouns, Types, Morphisms

    2023-Feb-03 picking up from tweet thread of 220909  AxLam model: Noun (space), Type (paint), Morphism (arrow) AxLam is for writing models using [concepts, types, and morphisms].  Our concepts may be in the form of some data, or less specifically as things we choose to name or refer to in a model.  Over this concept space, we use types and morphisms to define an adjustable descriptive model that directs and regulates processing of the concept data (or other manifestation).  Alternatively and  more approachably we may write in terms of [nouns,  formal classes, and mappings], and this framing is mostly equivalent for informal purposes. Nouns / Concepts / Terms / Data Nouns (i.e. concepts) describe anything we wish to refer to, and need not be explicit or named.  We think of nouns as the space of things we might try to describe, name or refer to.  "Terms" in a type-theoretic sense are nouns.  Real things in the human world that someone cares about are nouns.  In practice when we
    Read more

    AxioMagic under Spark on cloud (AWS, Azure, ...)

    AxioMagic under Spark on ${ cloud  } AxioMagic relies on functional composition over immutable inputs, thus matching modern evaluation frameworks like Apache Spark, which defines a structured approach to managing data contexts of functional evaluation over data frames.  Spark embodies a refinement of both  ETL and MapReduce methodology.  State machines like Spark require computation and storage resources which may come from any cluster, but today are commonly provided from cloud environments, yielding high volume functional computation at predictable usage-based costs.  We especially value Spark for open scientific dataset analysis, where it is common to work with large data files in interchange formats. Essential features of Spark distributed evaluation Spark assembles batch pipelines to pump datasets of structured records through functional tasks (which may  invoke side-effects, with all necessary stipulations).  This pipeline serves to evaluate a given distributed functional algorit
    Read more