walker (Apr 14 2023 at 14:59): walker (Apr 14 2023 at 14:59):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?
Gaëtan Gilbert (Apr 14 2023 at 15:05):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.
Patrick Nicodemus (Apr 14 2023 at 15:07):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
walker (Apr 14 2023 at 15:17):That is strange, I always knew that ocaml (unlike Haskell) didn't allow general recursion and only structurally decreasing recursions were allowed
Enrico Tassi (Apr 14 2023 at 15:29):let rec f x = f x typechecks
Ali Caglayan (Apr 14 2023 at 16:50):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: Oct 13 2024 at 01:02 UTC