Here are a few observations about the set comprehension syntax in HOL Light and
HOL4.
The HOL4 Description manual says that {t | p} parses to: GSPEC(\(x1,. .
.,xn).(t,p)) where x1, . . . , xn are those free variables that occur in both t
and p. It also says that it is an error if there are no such
Hi Rob,
The code for HOL4 set abstractions says that the bound variables
of a set abstraction {t | p} are the intersection of the free variables
of t and p unless either side has no free vars, in which case the
bound variables are those of the other side. Also, if t has no free vars,
then fail.
Konrad,
On 29 Dec 2013, at 17:31, Konrad Slind wrote:
> Hi Rob,
>
> The code for HOL4 set abstractions says that the bound variables
> of a set abstraction {t | p} are the intersection of the free variables
> of t and p unless either side has no free vars, in which case the
> bound variables
Rob,
On 29 Dec 2013, at 21:26, Rob Arthan wrote:
>> The code for HOL4 set abstractions says that the bound variables
>> of a set abstraction {t | p} are the intersection of the free variables
>> of t and p unless either side has no free vars, in which case the
>> bound variables are those of
Rob, I learned a lot from your post! My conclusion is that in both HOL Light
and HOL4,
{f x | R x} = λa. ∃x. R x ∧ a = f x
for some variable a than is not free in R x or f x. I judge both HOL
approaches to have pluses & minuses, and can't rate one above the other:
1) In HOL Light, the proof o
Bill,
On 1 Jan 2014, at 03:04, Bill Richter wrote:
> Rob, I learned a lot from your post! My conclusion is that in both HOL Light
> and HOL4,
> {f x | R x} = λa. ∃x. R x ∧ a = f x
> for some variable a than is not free in R x or f x. I judge both HOL
> approaches to have pluses & minuses, an
Rob, thanks for correcting my variable capture mistake:
In this case, the two instances of x have different types and there
is no variable capture, since two variables with the same name but
different types are considered to be distinct in the logic.
Right, and you have to do the type in
On 4 Jan 2014, at 6:17 pm, Bill Richter wrote:
> To see this, think of a mathematical function f: X ---> Y between sets and a
> subset A of X. Then we speak of the image f(A), which is a subset of Y,
> defined by
>
> f(A) = {f(a) | a ∈ A}.
>
> But what does that mean? I claim it's just a shor
Bill,
On 4 Jan 2014, at 05:17, Bill Richter wrote:
> So the expandsion order doesn't matter The real issue is that r is now free
> in (f x, R x), unlike the first example.
Yes. My explanation of the phenomena you were observing was wrong.
>
> Why do you need to calculate it?
>
> We don't ne
Bill,
> On 4 Jan 2014, at 05:17, Bill Richter wrote:
...
On 7 Jan 2014, at 16:22, Rob Arthan wrote:
> I think we will just have to agree differ about this. Let me just make two
> comments:
>
Something very odd happened with my e-mail client which caused it to discard the
two comments. They wer
Not wanting to be too picky here (because I very much agree with the thrust
of what Rob is saying), but isn't ProofPower term quotation parsing
sensitive to the subgoal package state (specifically, free variables in term
quotations pick up the types of existing free variables in the subgoal
package
Mark,
On 8 Jan 2014, at 03:22, Mark Adams wrote:
> Not wanting to be too picky here (because I very much agree with the thrust
> of what Rob is saying), but isn't ProofPower term quotation parsing
> sensitive to the subgoal package state (specifically, free variables in term
> quotations pick up
Ah yes, point taken.
on 8/1/14 10:13 AM, Rob Arthan wrote:
> Mark,
>
> On 8 Jan 2014, at 03:22, Mark Adams wrote:
>
>> Not wanting to be too picky here (because I very much agree with the
> thrust
>> of what Rob is saying), but isn't ProofPower term quotation parsing
>> sensitive to the subgoal
Rob, I think Michael's IMAGE idea may show that I was wrong about your semantic
embedding idea. I said that I was happy with the HOL Light parser's definition
of the set comprension
{f x | R x} = {a | ∃x. a = f x ∧ R x}
and I didn't think that it made sense to talk about the semantic value of
14 matches
Mail list logo
