[opentheory-users] article format wording about constants

[Joe Hurd]

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.

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
>