User loginNavigation |
Type system based on epistemic modal logic?This is something I’ve been mulling over lately, and I’m curious to hear opinions on it and whether there’s any existing research (I couldn’t find any). Since type systems based on linear logic are receiving more attention lately in Rust and the forthcoming linear types extension for Haskell, I was looking around at different logics to see if they would make a useful basis for type system features in a programming language. I was aware of modal logics, but hadn’t really looked into them since I read From Löb’s Theorem to Spreadsheets a few years ago. I came across epistemic modal logic, a logic for reasoning about knowledge. That struck me as potentially very useful for distributed data stores, in which different agents (servers) know different things (have different data), and also know things about the things that they and other agents know. For instance, if a client asks a server for some data, the server may be aware that it doesn’t have the data in question, by the “negative introspection axiom”, ¬Kiφ ⇒ Ki¬Kiφ, if an agent (i) does not know (¬Ki) some fact (φ), then that agent knows (Ki) that it does not know the fact (¬Kiφ). However, it may know that some other agent does know the fact, and can go and fetch it accordingly, or arrange for the other agent to send it directly to the client. This could incorporate other modalities such as possibility (◊), necessity (□), “everyone knows” (E), “common knowledge” (C), “distributed knowledge” (D). Just brainstorming, I feel like a type system based on these ideas might be able to enforce things like:
I’m just riffing informally here. Let me know your thoughts, or if you can point me to any resources. :) By Jon Purdy at 2017-08-09 20:55 | LtU Forum | previous forum topic | next forum topic | other blogs | 3784 reads
|
Browse archives
Active forum topics |
Recent comments
16 weeks 1 day ago
16 weeks 2 days ago
16 weeks 2 days ago
38 weeks 3 days ago
42 weeks 5 days ago
44 weeks 2 days ago
44 weeks 2 days ago
47 weeks 7 hours ago
51 weeks 4 days ago
51 weeks 4 days ago