How is does type theory (coq, lean, agda), and logic programming (prolog, datalog) differ from each other.

Logic programming is a way of declarative specifying an algorithm, using classical 1st order logic and the implementation of the computation of that algorithm does not have to be specified.

Type theory is a way of declarative specifying an algorithm, using constructive logic, making program synthesis possible.

  • 3
    $\begingroup$ It's not clear what you are trying to ask. "differerence between" doesn't mean anything in particular. Neither does "relate to". If 2 things involve different models of computation, so what? (Rhetorical.) If you don't know what 2 things are, why are you asking for "the difference"?--Find out what each is. If you think you know what they are, how is it that you need us to give "the difference"?--and what does that even mean? Either way give definitions, show & apply research & ask 1 clear specific non-duplicate question about how you are stuck. $\endgroup$ – philipxy Dec 6 '20 at 2:08
  • $\begingroup$ I agree with others; usually instead of asking what the difference is, it is worth to first understand each. If you understand each, you should be able to identify differences on your own. If you don't understand them, it's better to ask focused questions about one at a time. It's also a fallacy to expect there will be only one difference, so asking for "the difference" contains a faulty premise. $\endgroup$ – D.W. Dec 9 '20 at 6:35
  • $\begingroup$ We expect you to do a significant amount of research before asking (see our [help/how-to-ask]); then show us in the question what your understanding is, and give us some background on the topics. This will help us gauge your understanding, provide appropriate answers, and make the question more useful for others. $\endgroup$ – D.W. Dec 9 '20 at 6:35

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.