On Thu, Jun 20, 2019 at 11:20 AM Benoit <[email protected]> wrote:
> Answering Mario's test question: If I see "sum_ k e. A B" and I don't
> know the definition, then I will hope that A does not contain occurrences
> of k ;-) And if it does, then I would tend to think that the occurrences
> are bound, simply because k looks "dummy" in "k e. A", so the occurrences
> in A should, too. (I admit I don't know if it's the case or not, I would
> have to look at the definition.)
>
> Your example of the dependent Pi type is interesting. Do you have a
> concrete example where the "indexing set" depends on the index variable,
> and where it is important that the occurrence be free?
>
The only way this can occur (in DTT and metamath) is in the presence of
name shadowing. Most systems I know that have named variables also permit
name shadowing with the same behavior as metamath, i.e. inner binder wins.
So for example we could have the type
Pi (A : Type), Pi (x : nat), Pi (x : vector A x), list A
which would normally be written
Pi (A : Type) (x : nat), vector A x -> list A,
which might be the type of a function that takes a fixed length
vector/array and returns a list by forgetting the length. These two types
would normally be considered alpha equivalent, since the arrow is just
notation for a Pi that ignores its argument. If we interpreted "Pi (x :
vector A x)" where x was a vector of length x on the right, then it would
be total nonsense; the vector's length would be a vector whose length is a
vector... and you would have an infinite type (not to mention the fact that
it's not even well typed).
Your other examples (nlab, bounded Zermelo, many-sorted logic) are very
> interesting. They show that we should really avoid using the degenerate
> instance of df-opab and instances of df-ral where A contains occurrences of
> x, etc. Since you are fine with it, if Norm agrees, I would like, as
> proposed in my previous message, to discourage use of df-ral, df-opab,
> etc., to deduce from them dfral, etc. which are identical but have a dv
> condition, and to use only the latter. Would this help for your
> translation project?
>
By the way, the translation project is basically done already. Like I said,
these are lessons learned from looking at metamath in a different notation.
The translation will work with or without this change; the difference is
that the translation itself, expressing the external semantics of the
metamath constant, better accords with what we would normally expect in the
target language. Said another way, when asked to define "restricted forall"
in a HOL language, we invariably end up with a certain definition; if the
metamath concept by the same name has a significantly different definition
we should examine why that is and see which definition makes more sense
from both points of view.
> I wrote above that Mario's proposal df-opab3 would yield
> |- { <. x , x >. | x = 2 } = { z | E. x z = <. x , 2 >. }
> and I said that this was clearly false. Mario wrote:
> > This is intended behavior. I think we should probably more or less ban
> the use of { <. x , x >. | ph }, but when it is used, I want it to have
> this behavior; BOTH x's are new bound variables, and they are always bound
> in the order written, so the second x shadows the first and hence you can
> rename the "outer" one to get { <. x , x >. | x = 2 } = { <. y , x >. | x =
> 2 }. I think that using { <. x , x >. | ph } to mean a subset of the
> diagonal is a horrible hack because it implies a flexibility on the left of
> a set comprehension that we don't actually have, and it breaks the pattern.
> If you have the general rule "all multiple binders are bound from left to
> right" you can guess this behavior without having to read the definition
> (assuming you realize that { <. x , y >. | ph } is a syntax constructor in
> the first place, rather than the composition of <. x , y >. and a
> nonexistent { A | ph }.)
>
> I agree that writing { <. x , x >. | ph } is a hack (albeit not a horrible
> one), for the reasons you wrote. The thing is that we write this
> informally very often, and everyone understands it as some subset of the
> diagonal. Therefore, I agree that we should avoid/discourage or even ban
> it, but if this has to be defined, then it should really denote the
> intended subset of the diagonal. It looks like on this last point, we have
> a deep disagreement, due to our different backgrounds.
>
I admit that I felt the same way about this until I noticed this behavior
and thought about the actual binding semantics here. I want this to act
more like A. x A. y ph in terms of binding structure; the weirdest part
with this notation is that the binders are crafted to look like a pair
(even though it's not a pair), so when you read <. x , x >. you think it's
a diagonal pair. But that's a misreading because the two halves of the pair
are in different scope; the first x refers to the (just introduced) left
variable and the second x refers to the (again just introduced) right
variable. Again, compare this to A. x A. x ph to see why this might be
reasonable behavior.
This would be a lot less confusing if we had an actual general notation
such as { A | x | ph } and { A | x , y | ph }. I'm still not completely
sold on this style either, because A is to the left of the variables that
bind it, but this solves the issue of the "split pair". If you have { <. x
, x >. | x , x | ph }, then using the same binding semantics, the first
variable is shadowed by the second so you can alpha rename to { <. x , x >.
| y , x | ph }, which is indeed a subset of the diagonal.
Mario
--
You received this message because you are subscribed to the Google Groups
"Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to [email protected].
To view this discussion on the web visit
https://groups.google.com/d/msgid/metamath/CAFXXJSv3UdDYDVxH8LoDhQiZT64B7D%3DY1nEC2BR1gtXB-Z7YOQ%40mail.gmail.com.
