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
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
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 were
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
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
On 4 Jan 2014, at 6:17 pm, Bill Richter rich...@math.northwestern.edu 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
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, and
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
Rob,
On 29 Dec 2013, at 21:26, Rob Arthan r...@lemma-one.com 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
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
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.
11 matches
Mail list logo
