Gergely Buday (Aug 18 2020 at 13:14): Gergely Buday (Aug 18 2020 at 13:14):Paulson writes in Isabelle a Generic Theorem Prover that
"A term t can be certified under a signature to ensure that every type in t is declared in the signature and every constant in t is declared as a constant of the same type in the signature. ..."
Am I right to state that a certified term is like a closure in programming language theory, having all the free variables declared besides the term?
Manuel Eberl (Aug 18 2020 at 13:37):No I don't think free variables enter into it. You can make cterms with undeclared free variables. The important thing is that each cterm is well-typed with respect to a specific underlying theory
Manuel Eberl (Aug 18 2020 at 13:38):and it "knows" which theory that is
Manuel Eberl (Aug 18 2020 at 13:38):so all the constants that appear in the term are actual constants in the theory, and their types are consistent with the types with which they were declared
Manuel Eberl (Aug 18 2020 at 13:41):You can do pretty crazy things with free variables; you can even make a term that has two occurrences of an undeclared free variable x in it, once with type bool and once with type nat. These are considered different variables by the kernel, if I recall correctly. But there is no inconsistency, and the higher up levels of Isabelle usually prevent you from doing such things in order to prevent confusion.
ML_val ‹
HOLogic.mk_prod (@{term "x :: nat"}, @{term "x :: bool"})
|> Thm.cterm_of @{context}
›
On a practical level, I think of term as ‘pre-terms’. They are the thing that you usually manipulate in ML, but they might (in principle) be ‘broken’ (i.e. there might be type errors in them if you're not careful). When you want to actually make a theorem involving them, you have to turn them into a cterm. Conversely, when you get a cterm somewhere, the first step is usually to just turn it into a regular term. The only exception is when performance matters; then you will try to avoid having to recertify terms, because it's expensive.
Gergely Buday (Aug 18 2020 at 14:42):Then it is a type-checked term against a theory, I see, thanks.
Last updated: Dec 21 2024 at 16:20 UTC