7
$\begingroup$

In CMU's HoTT course, lecture 1, which can be found here: https://scs.hosted.panopto.com/Panopto/Pages/Viewer.aspx?id=0945cc7f-48b7-4803-81af-e7193a3f461d

At 33:52, Harper was giving parallel comparison between synthetic theories and analytic ones, and when he reached PL theory, he said Coq is analytic and said Coq only proves a language in its grammar but not the parser itself.

I have a strong desire to disagree somehow but I don't have a clear idea why I would want to do that. I believe that Coq is very synthetic, so are any other proof assistants based on dependent type theory, because all these languages do nothing but build programs. We can also express axiomatic algebra in Coq by using type classes for example, and concretize whenever suitable. This pattern is especially the case in Agda.

So my question is, was Harper right? If he's right, which part of my view causes my misunderstanding?

$\endgroup$
11
$\begingroup$

The remark is about one specific usage of Coq, namely formalization of programming language theory.

Let us first make clear the distinction between synthetic and analytic:

  • In a synthetic approach to a subject we say that there are things whose basic properties and structure are postulated in one way or another. We then study these things by relying only on the postulated properties and structure.

  • In an analytic approach to a subject we discover that there are certain things. To learn more about them, we take them apart, we study how they are made and we analze them. This way we discover their properties and structure.

How would one study a programming language in these two ways?

Synthetically, we would postulate the constituent parts of the language (there are terms, there are types), their basic structure (these are the ways of building terms) and basic properties. We do not ask what the terms and type are made of, or whether the terms are trees or strings, or whether the collection of types is built in a particular way.

Analytically, we would start with a mathematical setup that allows us to do many things, such as use inductive definitions to construct mathematical objects. We woudl build terms and types as particular inductively defined sets or types. Then we would study their structure, how we can transform them, etc.

It should be clear that Coq is of the analytic kind. When you implement a programming language in Coq, you define inductive types of terms and types. Then you analyze them using induction, define operational semantics as a recursive function on the syntax of terms, etc.

On the other hand, Twelf is of the synthetic kind. We postulate that there is a type of terms and a type of types, but we do not tell Twelf that these are inductive types (there's no way to say that in Twelf). We define operational semantics by providing basic transition rules. There is no mention of recursively defined functions (there's no way to define functions in Twelf), we just rely on the postulates that we wrote down.

You should compare the above situation to planar geometry. Hilbert's approach to geometry is synthetic (but his ideas are rooted in Euclid), Descartes' are analytic. The analytic geometry is so called because a line is not a primitive concepts: it has an inner structure, namely it is a set of points.

$\endgroup$
  • $\begingroup$ Thank you for your answer. Could you see if my following statements aligned correctly to check my understanding? 1. It's still possible to do synthetic approach in Coq, which is taken, say, by Unimath, by disallowing use of inductive definitions. 2. The study of type theories itself is synthetic, but the study based on them (assuming freely use of language feature) would be analytic. If HoTT is implemented as a programming language, the use of HIT and induction would effectively make it an analytic study. $\endgroup$ – Jason Hu Jun 14 '18 at 19:39
  • $\begingroup$ Unimath is synthetic not because it disallows inductive types, but because it speaks about homotopy types without analyzing what they're made of. $\endgroup$ – Andrej Bauer Jun 14 '18 at 20:37
  • $\begingroup$ @AndrejBauer - Oddly, this distinction appears to be just the opposite of that in philosophy, including philosophy of mathematics. There, "analytic" means statements whose meaning depends solely on the terms and their relations, without having to add in, "synthesise", any external input (eg factual knowledge about the state of the world). So on this usage, Euclid would be analytic, while Descartes would involve synthesizing geometric notions with algebraic notions (eg a point is a pair (x,y) and a line is an equation y = mx + b). $\endgroup$ – Diagon Jun 21 '18 at 7:40

Your Answer

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

Not the answer you're looking for? Browse other questions tagged or ask your own question.