[opentheory-users] article format wording about constants

[Ramana Kumar]

On Sat, Jan 15, 2011 at 11:17 PM, Joe Hurd <joe at gilith.com> wrote:
> Hi Ramana,
>
> The example I gave make deliberate use of the universal quantifiers to
> illustrate my point about variables being determined by both name and
> type. As you found out, without any binders HOL4 does indeed identify
> the variables, but this can be seen as a 'forced additional
> specialization': it is always sound to identify free variables in a
> theorem but a logical weakening may occur as a result.

Does OpenTheory's subst command also do renaming of bound variables
where necessary?
It might be nice to document that; your call though.
I was about to say I want to know how the new names are to be
computed, but I realize that since they are bound, it doesn't matter.

>
> Cheers,
>
> Joe
>
> On Sat, Jan 15, 2011 at 3:10 PM, Ramana Kumar <ramana.kumar at gmail.com> wrote:
>> 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
>>>>>>
>>>>>
>>>>
>>>
>>
>> _______________________________________________
>> opentheory-users mailing list
>> opentheory-users at gilith.com
>> http://www.gilith.com/opentheory/mailing-list
>>
>
> _______________________________________________
> opentheory-users mailing list
> opentheory-users at gilith.com
> http://www.gilith.com/opentheory/mailing-list
>