Semantic data fuels many different applications, but is still lacking proper integration into programming languages. Untyped access is error-prone while mapping approaches cannot fully capture the conceptualization of semantic data. In this paper, we present λ_DL, a typed λ-calculus with constructs for operating on semantic data. This is achieved by the integration of description logics into the λ-calculus for both typing and data access or querying. It is centered around several key design principles, in particular: (1) the usage of semantic conceptualizations as types, (2) subtype inference for these types, and (3) type-checked query access to the data by both ensuring the satisfiability of queries as well as typing query results precisely. The paper motivates the use of a designated type system for semantic data and it provides the theoretic foundation for the integration of description logics as well as the core formal definition of λ_DL including a proof of type safety.

Key propositions of λ_DL

• Use Concepts as types:  Type safety can only be achieved if terms are typed precisely. This is only possible if the conceptualizations of semantic data are usable in the programming language. Therefore, concept expressions must be seen as types in the language.
• Use Subtype inferences: Due to the large number of potential concepts, it is infeasible to precompute subtype relations. Therefore, the facts about subsumptive relationships between concepts must be added to the system during the type checking process by forwarding these checks to the knowledge system.  
• Typing of queries: To avoid runtime errors, queries must be properly type-checked. Queries can be checked in two ways: First, unsatisfiable queries must be rejected. Queries for which no possible A-Box instance can produce a result are therefore detected and rejected.  Second, usage of queries must be type safe, meaning that the query result must be properly typed. Queries always return lists in λ_DL.
• DL-safe queries: A knowledge system might introduce anonymous objects to satisfy axioms. In the worst case, this can lead to infinitely large query results. However, very little information can be gained of such objects aside from their existence. λ_DL relies on a simplified form of DL-safe queries. Queries are enforced to be finite by only allowing unifications with known objects, even though this may also lead to empty result sets for queries.
• Open-world querying: When looking at inferencing, axioms may be true, false or unknown. For simplicity, λ_DL considers axioms to be true only if the axiom is true in all models. In other cases, the axiom is considered false.

Papers and Talks about λ_DL

• Programming with Semantic Broad Data (Presentation)
• λ_DL: Syntax and Semantics (Preliminary Report)

Prototypical implementation

A prototypical implementation of λ_DL has been created in F#. The implementation uses F# to encode evaluation and typing semantics, while relying on a knowledge base for inferencing. HermiT, a state of the art OWL reasoner, is used for this. However, since HermiT is only available in Java, a wrapper program needs to be used that interfaces with the F# implementation via command line. Therefore, the actual reasoning is done in a Java program while the parsing, evaluation and typing are coded in F#.
Further information can be found in the readme files.

(Source code | Precompiled) (last modified: 18.10.16)

Developers

Martin Leinberger

• Alumnus