So I know having a type checking algorithm is equivalent to proving strong normalization.

And there is type checking algorithm for coq in ocaml, but Ocaml does not allow general recursion, and Ocaml is logically weaker than coq, so how was it done?

Ocaml does not allow general recursion

this is wrong though

So I know having a type checking algorithm is equivalent to proving strong normalization.

only if the algorithm is proven to terminate. ocaml functions do not include proofs of termination.

I think it's inaccurate that Ocaml does not allow general recursion. I actually don't know anything about Ocaml here but it's possible you might be thinking of structural recursion on algebraic datatypes, but Ocaml allows other kinds of computation and control flow than this. Ocaml is a general purpose programming language and pretty much all general purpose programming languages are Turing complete and allow general recursion

That is strange, I always knew that ocaml (unlike Haskell) didn't allow general recursion and only structurally decreasing recursions were allowed

`let rec f x = f x`

typechecks

You might be confusing the fact that OCaml is based off of (higher order) System F which can be thought of as propositional logic with higher order quntaifiers except for first order. Hence is logically weaker than full higher order logic (i.e. Coq). However OCaml is only based off of System F and is not literally it. As a logic, OCaml has many ways to construct inconsistencies and this is nothing special since most good programming languages are inconsistent as logics, otherwise nothing would ever be done.

Last updated: Jun 16 2024 at 01:42 UTC