The n-Category Café

It might be fun to look into connections between dependent type systems and logic-based query languages.

Some well-known examples of what I mean by logic-based query languages:

• Relational calculus
• Datalog
• λProlog

These are listed in order of increasing expressiveness, and λProlog is Turing-complete, so may be too different from natural language questions. But λProlog also seems the closest of the 3 to type theory. And I think logic programmers still have something called “queries”. (The goal clauses, I think.) None of these use dependent types.

(I figure the main threat to your program of basing philosophy on dependent type theory is not that it’s not powerful enough, but that it could appear to be an unnecessary complication. In programming languages too, many problems are successfully addressed without dependent types.)

You might try talking to Neel Krishnaswami about this. He has a blog post about a variant of Datalog he worked on, using some type systems ideas. (And he’s a type theorist who’s commented on this blog before.)

Twelf (stubby article on the nLab) is the only example I know of of a tool based on dependent types, and with a focus on logic programming. But other dependent type systems support it, via propositions-as-types and proof search.

I often mentally classify questions into yes-or-no questions (which ask for just a truth value), questions whose answer is an element of some well-defined set, and still more open-ended questions.

I like to ask yes-or-no questions, because I hope most people have the patience to at least give me one bit of information. But in practice, most people take these questions as a request for a long rambling discussion. I like answering yes-or-no questions when they’re well-formed. But in practice, they often involve mistaken presuppositions that prevent a simple answer. I suppose these are flip sides of the same coin! It reminds me of Nabokov, who complained of his apartment building where the neighbor downstairs had oversensitive ears and the one upstairs had feet of lead.

At the opposite extreme from a yes-or-no question, I hate getting questions in my email like “how does quantum entanglement work?”, where an answer would require guessing what the questioner knows or can understand.

I agree that (1) is a case of (2), and that (2) is a case of (3). I also think (4) can be regarded as a case of (3) by combining the questions with tuples, e.g. $(Wh x:A)(Wh y:B) R(x,y)$ should be equivalent to $(Wh p:A\times B) R(p)$.

One might argue that (5) is also reducible to (3) by introducing a “type of reasons”, just as when encoding logic in type theory we represent a proposition by its “type of proofs”.

This general form of question (3) looks similar to the posing of a problem in a programming language: $A$ is the (simple) type of a function and $B$ is the specification it has to satisfy. (Similarly, in mathematics, we might have to define an object that satisfies some desired property.) Defining the function is answering the question; then proving the specification is justifying the answer, which could be considered to be answering a particular kind of “why” question: “why does $x$ have property $B$?”. Of course in a dependently typed language one can do both at once by constructing an element of $\sum_{x:A} B(x)$; I suppose in natural language one might end a wh-question with “and why?”.

Programming languages can do these “which?” selections (SQL is designed for them). The theory of relational databases has been a big field in CS since the 70s, and the industry standard language is SQL. As David mentions in his post, there is a subarea overlapping logic, philosophy of language and science, which looks at questions and tries to analyse what they are.

Outside of SQL, in R, one has the which() command, which returns the indices of a given argument vector satisfying the stated condition. (Though I don’t use Python or C++ much, they have similarly functionality.) E.g., if I assign the vector $(0,1,0,1,1,0,1,1,1,0)$ to $A$, like this,

$A \leftarrow c(0,1,0,1,1,0,1,1,1,0)$

then the command

$which(A \text{ == } 1)$

gives the indices,

$\text{2 4 5 7 8 9}$

I wondered if I could embed a function, $B$ to specify the condition:

$A \leftarrow c(0,1,0,1,1,0,1,1,1,0)$

$B \leftarrow function(x) \ \{ \ x \ \text{ == } \ 1 \ \}$

The function $B$ gives $\top$ if the input is 1, and $\bot$ otherwise.

Then the command,

$which(B(A))$

gives the same answer as before (i.e., answers “which (indices for) elements of $A$ satisfy $B$?”).

I found your book “Modal Homotopy Type Theory” extremely useful and inspiring for developing the theory for strong AI. My approach is based on combining classical logic-based with deep learning. An interesting insight I got is that Google’s BERT, a deep-learning language model, can actually be viewed as an alternative form of logic via the Curry-Howard correspondence.

Another idea I have is that fuzzy logic may be viewed as a logic living on HoTT’s level 0 (the level of sets), where truth values are not just {0,1} but a real number in [0,1] depending on the ratio of set elements belonging or not belonging to some predicates. This explains why “mere propositions” have binary truth values.

(Sorry about the digressions…)

Re the issue of questions, I think it would be helpful to consider what is the nature of having a “question” in the mind of an intelligent system. Clearly this would be part of the mental “state” of the intelligent agent. Traditionally we think of the AI system’s state as constituted of logic propositions. Perhaps what you need here is to expand the scope to beyond traditional propositions (as “things that can be assigned truth values”). A question would be like a desire or a goal, which suggests the realm of planning and actions. Interestingly, again by the Curry-Howard correspondence, actions may be regarded as side-effects of programming.