[opentheory-users] article format wording about constants

[Ramana Kumar]

Actually, I see this phrase in the HOL4 documentation for INST_TYPE:

"Variables will be renamed if necessary to prevent distinct variables
becoming identical after the instantiation."

So it would seem there is a bug in whatever version of HOL4 I happen
to have built at the moment... (which may be one whose kernel I was
playing around with... will continue this thread on a HOL4 list if
necessary)

At least the documentation of INST_TYPE matches your description of a
fundamental difference between constants and variables :)


On Sat, Jan 15, 2011 at 9:50 PM, Ramana Kumar <ramana.kumar at gmail.com> wrote:
> On Sat, Jan 15, 2011 at 9:41 PM, Ramana Kumar <ramana.kumar at gmail.com> wrote:
>> On Sat, Jan 15, 2011 at 9:13 PM, Joe Hurd <joe at gilith.com> wrote:
>>> Hi Ramana,
>>>
>>>> What does the phrase "with definition ..." mean in the article format spec?
>>>> In my opinion it doesn't add anything except potential confusion.
>>>
>>> I agree that the "with definition ..." language is more confusing than
>>> helpful, and I've removed it from the article format spec.
>>>
>>>> However, notice the asymmetry: const takes 1 argument, constTerm takes
>>>> 2, but var takes 2 arguments and varTerm takes 1. Surely constants
>>>> should act more like variables?
>>>
>>> This asymmetry is deliberate, and reflects a fundamental difference of
>>> constants and variables. Constants are determined just by their name,
>>> but variables are determined by their name and type. This is
>>> illustrated by the theorems
>>>
>>> |- !(v : 'a list) (v : bool list). P (v : 'a list) (v : bool list)
>>>
>>> |- P (c : 'a list) (c : bool list)
>>>
>>> Applying the type instantiation ('a |-> bool) to both results in
>>>
>>> |- !(v : bool list) (v' : bool list). P (v : bool list) (v' : bool list)
>>>
>>> |- P (c : bool list) (c : bool list)
>>>
>>> where the two constants have been identified, but the two variables
>>> have been kept separate.
>
> This is not true in HOL4.
> The following does not raise Bind:
>
> val P = mk_var("P",``:'a list -> bool list -> bool``)
> val va = mk_var("v",``:'a list``)
> val vb = mk_var("v",``:bool list``)
> val Pvv = list_mk_comb(P,[va,vb])
> val Pvv = mk_thm([],Pvv)
> val false = let
>  val (_,[va,vb]) = strip_comb(concl Pvv)
> in va = vb end
> val Pvv' = INST_TYPE [alpha|->bool] Pvv
> val true = let
>  val (_,[va,vb]) = strip_comb(concl Pvv')
> in va = vb end
>
>
>>
>> So why does constTerm take 2 arguments instead of just 1?
>> Is it just to allow you to instantiate type variables that might be in
>> the constant on the stack?
>>
>>>
>>>> Also, it's not clear whether a "new constant" with the same name as a
>>>> previously defined constant is allowed. I presume so.
>>>
>>> This is left to the system, which must be careful to disallow
>>>
>>> define `c = T`
>>> define `c = F`
>>> prove `T = F`
>>>
>>> I believe all of the HOL theorem provers maintain a symbol table of
>>> constants, and will not allow redefinitions with the same name. The
>>> logical kernel of the opentheory tool stores the definition with the
>>> constant, so will happily allow redefinitions with the same name
>>> (because the two "c" constants above will be treated as different
>>> constants).
>>
>> HOL4 allows redefinitions with the same name and marks the old
>> constant as "old"; only constants that aren't so marked can appear in
>> any saved theory segment, but while developing a segment it enables
>> one to redefine the same constant many times. You wouldn't be able to
>> prove `T = F` as above, though, because the theorem equating `c = T`
>> would be turned into `OLDc = T` when `c` is redefined, effectively
>> making the old one a different constant. This is similar to
>> opentheory, except the marks don't know anything about the definition
>> of the constant, they're essentially just timestamps.
>>
>> So I think if while recording an OpenTheory article from HOL4 if you
>> redefine a constant, the right thing will happen: both systems will
>> treat the new constant as different from the old, even though it has
>> the same name.
>>
>>>
>>> Cheers,
>>>
>>> Joe
>>>
>>> _______________________________________________
>>> opentheory-users mailing list
>>> opentheory-users at gilith.com
>>> http://www.gilith.com/opentheory/mailing-list
>>>
>>
>