Email Gateway (Aug 23 2022 at 09:02): Email Gateway (Aug 23 2022 at 09:02):From: Manuel Eberl <eberlm@in.tum.de>
Hello,
I just noticed something odd. When a polymorphic constant has sort
constraints, you normally cannot write it down with its type
instantiated to a type that does not fulfil these constraints. For
instance, term ‹-1 :: nat› or @{cterm "-1 :: nat"} do not work because
"nat" does not have the sort "uminus".
However, when one constructs the term in ML and then certifies it with
Thm.cterm_of, it works:
ML_val ‹
let
val t =
Const (@{const_name "uminus"}, @{typ "nat ⇒ nat"}) $ @{term "1 :: nat"}
in
Thm.cterm_of @{context} t
end
›
This outputs
val it = "- (1::nat)": cterm
It's not a soundness problem, but I still find this behaviour somewhat
unexpected. I would naïvely have thought it would be impossible to get
the natural number "-1". Is this intended? Is this for performance reasons?
(For those wondering why this is okay on a logical level, the negation
operator is essentially acting as an unspecified function, so "-1 ::
nat" is not /actually/ -1, but it is equal to some "proper" natural
number, we just don't know which one)
Manuel
Email Gateway (Aug 23 2022 at 09:02):From: Makarius <makarius@sketis.net>
On 29/05/2020 12:00, Manuel Eberl wrote:
I just noticed something odd. When a polymorphic constant has sort
constraints, you normally cannot write it down with its type
instantiated to a type that does not fulfil these constraints. For
instance, term ‹-1 :: nat› or @{cterm "-1 :: nat"} do not work because
"nat" does not have the sort "uminus".However, when one constructs the term in ML and then certifies it with
Thm.cterm_of, it works:ML_val ‹
let
val t =
Const (@{const_name "uminus"}, @{typ "nat ⇒ nat"}) $ @{term "1 :: nat"}
in
Thm.cterm_of @{context} t
end
›
That is the normal expected behaviour: sort constraints for constants are
merely an extra sanity check in abstract syntax (Syntax.check operations), but
have no relevance for the logic.
Even more, there can be additional type constraints for constants that
Syntax.check will observe, but Thm.cterm_of doesn't.
Is this for performance reasons?
No, it is to get concepts right and have an implementation that fits to these
concepts. Arriving there has required many years, approx. from 1994 to 2008.
(For those wondering why this is okay on a logical level, the negation
operator is essentially acting as an unspecified function, so "-1 ::
nat" is not /actually/ -1, but it is equal to some "proper" natural
number, we just don't know which one)
Conventional logic can always have terms that are uninterpreted or "non-denoting".
Makarius
Last updated: Apr 26 2024 at 12:28 UTC