[opentheory-users] article format wording about constants

[Ramana Kumar]

Argh... the HOL4 Logic manual has this instead:

"After the instantiation, variables free in the input can not become bound, but
 distinct free variables in the input may become identified."

I don't know what to believe any more.

On Sat, Jan 15, 2011 at 9:56 PM, Ramana Kumar <ramana.kumar at gmail.com> wrote:
> 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
>>>>
>>>
>>
>