Parameters and strings

[fl]

I think that a way to represent the parameters of a function when there are more than 2 parameters is to use a
Words of definite length. (Mario Carneiro didn't select this proposal but a word of  identified length has its merits.
Here, in the case of parameters for instance.)

You may have:

( f e. ( RR Words 4 ) |-> ( ( f ` 1 ) + ( f `2 ) ) * ( ( f ` 3 ) + ( f `4 ) ) )

You no longer need to extract the variables with "E." or with a bunch of "dom" or "cod".

You might also use predicates to express a String.

String 4 RR CC + Intvl = { <. 1 , RR >. , <. 2 , CC >. , <. 3 , + >. } u. { <. 4 , Intvl >. }

String 5 RR CC + Intvl (/) = { <. 1 , RR >. , <. 2 , CC >. , <. 3 , + >. } u. { <. 4 , + >. , <. 5 , (/) >. }

(The 4 and 5 here are to distinguish two constructs. I have not checked if it is possible in Metamath. If not
we can say String4, String5 up to 9.)

The "String" construct is definitely shorter. It is very useful in logic for instance.

We can also consider the first element of a String contains the size of the string

String 4 RR CC + Intvl = { <. 0 , 4 >. , <. 1 , RR >. , <. 2 , CC >. } u. { <. 3 , + >. } , { <. 4 , Intvl >. }

Then the siae may be retrieved by a function that uses the string as its parameter.

I know that Norm doesn't like predicates. For three reasons:

1) Other proof systems don't use class variables. And compatibility is then not insured.
It is a very good reason indeed. Especially because Mario will be annoyed by this in his
work of translation. Right.

2) Set theory, as suggested by its name is about sets. Everything in mathematics can be expressed by sets.
(Seems a philosophical matter for me.)

3) We need to add theorems of the hb* form when we use. (It is true.)

But I also think we need a construct like strings.

For instance if you need to express the concept of betweenness in Euclid's planar geometry, to say
that B is between A and C either you write B e. ( A btw C ) or  (other solution) <. <. A , B >. , C >. >. e. btw
But I think the easiest and more readable solution is something like String 3 A  B C e. btw. Obviously if you
don't want to be annoyed by the meaning of the symbol String you can replace this symbol by a innocuous one:
¤ for instance: ¤ 3 A  B C e. btw.

I think we might think about the idea of strings for a while.

--
FL

[Mario Carneiro]

On Thu, Feb 25, 2016 at 7:01 AM, 'fl' via Metamath <meta...@googlegroups.com> wrote:

I think that a way to represent the parameters of a function when there are more than 2 parameters is to use a
Words of definite length. (Mario Carneiro didn't select this proposal but a word of  identified length has its merits.
Here, in the case of parameters for instance.)

You may have:

( f e. ( RR Words 4 ) |-> ( ( f ` 1 ) + ( f `2 ) ) * ( ( f ` 3 ) + ( f `4 ) ) )

For now, a way to write this is e.g.

( f e. ( RR ^m ( 1 ... 4 ) ) |-> ( ( f ` 1 ) + ( f `2 ) ) * ( ( f ` 3 ) + ( f `4 ) ) )

or

( f e. ( RR ^m ( 0 ..^ 4 ) ) |-> ( ( f ` 0 ) + ( f `1 ) ) * ( ( f ` 2 ) + ( f `3 ) ) )

If there is a reason for the "4" to be variable, I would recommend not using either (0 ..^ N) or (1 ... N) in favor of I e. Fin, which allows for using either one, or other index sets like cartesian products, without any extra work.

If there are many parameters but they are all "named" so that there is no chance of varying the number of parameters as in the above, consider putting them all into a structure and name the structure extractors appropriately, e.g.

( f e. Gizmo |-> ( ( foo ` f ) + ( bar ` f ) ) * ( ( baz ` f ) + ( quux ` f ) ) )

You might also use predicates to express a String.

String 4 RR CC + Intvl = { <. 1 , RR >. , <. 2 , CC >. , <. 3 , + >. } u. { <. 4 , Intvl >. }

String 5 RR CC + Intvl (/) = { <. 1 , RR >. , <. 2 , CC >. , <. 3 , + >. } u. { <. 4 , + >. , <. 5 , (/) >. }

(The 4 and 5 here are to distinguish two constructs. I have not checked if it is possible in Metamath. If not
we can say String4, String5 up to 9.)

The "String" construct is definitely shorter. It is very useful in logic for instance.

The first construct is not possible, one is at the level of syntax parsing while the other is an interpretation of a class variable. Is "String N" a valid class? What about "String N A"?

The second construct is, with String1, ..., String9, but I think it would look nicer if we did this more similar to ordered pairs/triples, for example

<" A "> = ( snword ` ( _I ` A ) )

<" A , B "> = ( <" A "> concat <" B "> )

<" A , B , C "> = ( <" A , B "> concat <" C "> )
...

There are probably good arguments to extend this further, perhaps as far as 9 arguments (provided it actually gets used), which should be okay as long as there aren't too many theorems that are repeated 9 times.

We can also consider the first element of a String contains the size of the string

String 4 RR CC + Intvl = { <. 0 , 4 >. , <. 1 , RR >. , <. 2 , CC >. } u. { <. 3 , + >. } , { <. 4 , Intvl >. }

Then the siae may be retrieved by a function that uses the string as its parameter.

There is no reason to do this, since we can just use (#`S) to retrieve the length of a string.

 

I know that Norm doesn't like predicates. For three reasons:

1) Other proof systems don't use class variables. And compatibility is then not insured.
It is a very good reason indeed. Especially because Mario will be annoyed by this in his
work of translation. Right.

Don't worry about be being annoyed by any particular conventions used in metamath for translation purposes - I am already having to deal with the worst that is out there anyway.

 

2) Set theory, as suggested by its name is about sets. Everything in mathematics can be expressed by sets.
(Seems a philosophical matter for me.)

3) We need to add theorems of the hb* form when we use. (It is true.)

I would put it this way: there are good reasons to use a class predicate instead of a constant, but in most cases these reasons are not satisfied. Just make sure that you can explain your reasons. The most common reasons to use a class predicate is because either the argument or the return value is a proper class, or you want to make the syntax more pleasant.

 

But I also think we need a construct like strings.

For instance if you need to express the concept of betweenness in Euclid's planar geometry, to say
that B is between A and C either you write B e. ( A btw C ) or  (other solution) <. <. A , B >. , C >. >. e. btw
But I think the easiest and more readable solution is something like String 3 A  B C e. btw. Obviously if you
don't want to be annoyed by the meaning of the symbol String you can replace this symbol by a innocuous one:
¤ for instance: ¤ 3 A  B C e. btw.

With ordered triples the second option can also be written <. A , B , C >. e. btw, and with the alternative notation for strings above option three would be <" A , B , C "> e. btw. I prefer using a terminating token because it means you don't have to count arguments. Elsewhere I recommended a df-dec like notation such as "+ A "+ B "+ C (/), which has the advantage of being unbounded unlike the <" "> options, but on top of looking very strange it also yields a deeper tree (for the grammar parse), which is not necessarily a good thing. Breaking a long string into groups of 8, say, is likely to be more efficient than a long list one character at a time.

For betweenness specifically, I would actually recommend B e. ( A btw C ), since that way ( A btw C ) can be interpreted as the line segment from A to C. Better yet, I would prefer something like

$e |- W = ( btw ` K )

$p |- ( K e. Plig -> A e. ( B W C ) )

so that you can consider more general things that act like planar incidence geometries (like non-Euclidean geometry).

Mario

[fl]

The first construct is not possible, one is at the level of syntax parsing while the other is an interpretation of a class variable. Is "String N" a valid class? What about "String N A"?

   We would have:

   cs4 $a class String 4 A B C D $.

   cs5 $a class String 5 A B C D E $.

It is unambiguous. I've not checked if Meramarh allows that.

> I would put it this way: there are good reasons to use a class predicate instead of a constant,
> but in most cases these reasons are not satisfied. Just make sure that you can explain your reasons.

It is more compact to have String 6 A B C D E F than { <. 1 , A >.  ,  <. 2 , B >.  , <. 3 , C >.  , <. 4 , D >.  , <. 5 , E >.  , <. 6 , F >.  }. That's my main reason.

--
FL

[Mario Carneiro]

On Fri, Feb 26, 2016 at 4:10 AM, 'fl' via Metamath <meta...@googlegroups.com> wrote:

The first construct is not possible, one is at the level of syntax parsing while the other is an interpretation of a class variable. Is "String N" a valid class? What about "String N A"?

   We would have:

   cs4 $a class String 4 A B C D $.

   cs5 $a class String 5 A B C D E $.

It is unambiguous. I've not checked if Meramarh allows that.

Actually, on second thought this would work (allowable by metamath and the definition checker), since at this level the "4" is nothing more than a certain constant symbol, and is not being interpreted as a class. The only complexity arises in verifying grammar unambiguity, but this too is fairly simple.

 

> I would put it this way: there are good reasons to use a class predicate instead of a constant,
> but in most cases these reasons are not satisfied. Just make sure that you can explain your reasons.

It is more compact to have String 6 A B C D E F than { <. 1 , A >.  ,  <. 2 , B >.  , <. 3 , C >.  , <. 4 , D >.  , <. 5 , E >.  , <. 6 , F >.  }. That's my main reason.

And how do you feel about the proposed alternative <" A , B , C , D , E , F "> ?

 

Mario

[fl]

And how do you feel about the proposed alternative <" A , B , C , D , E , F "> ?

It looks also good. Except you have additional commas.

--
FL

[fl]

It looks also good. Except you have additional commas.

It looks good but it is not a function. You can't write "( f` ` 3 ) * ( f  ` 4 )" if f is a list of parameters to a function.
You need to extract the parameters with a lot of "E.", "dom" and "cod". It is the main drawback.

--
FL

[Jens-Wolfhard Schicke-Uffmann]

On Fri, Feb 26, 2016 at 04:18:32AM -0500, Mario Carneiro wrote:
>    We would have:
>    cs4 $a class String 4 A B C D $.
>    cs5 $a class String 5 A B C D E $.
>
> It is unambiguous. I've not checked if Meramarh allows that.
> Actually, on second thought this would work (allowable by metamath and the
> definition checker), since at this level the "4" is nothing more than a certain
> constant symbol, and is not being interpreted as a class. The only complexity
> arises in verifying grammar unambiguity, but this too is fairly simple.

Technically yes, but it would be very confusing, because if

String 4 A B C D

is a valid class, then people would generally expect also

String ( 2 + 2 ) A B C D

to be valid, but it wouldn't.

Regards,
Drahflow

[fl]

Technically yes, but it would be very confusing, because if

  String 4 A B C D

is a valid class, then people would generally expect also

  String ( 2 + 2 ) A B C D

to be valid, but it wouldn't.

Metamath will react. And soon people will understand they can't by checking the definition.

--
FL

[Mario Carneiro]

On Fri, Feb 26, 2016 at 4:53 AM, 'fl' via Metamath <meta...@googlegroups.com> wrote:

It looks also good. Except you have additional commas.

The additional commas are not necessarily a bad thing; especially if you get a long run of constants it can get very confusing, e.g.

String 4 1 <_ 4 2

does not mean what it looks like at first glance.

 

It looks good but it is not a function. You can't write "( f` ` 3 ) * ( f  ` 4 )" if f is a list of parameters to a function.
You need to extract the parameters with a lot of "E.", "dom" and "cod". It is the main drawback.

It is a function. In fact, it is a (Word`S). The only difference is that my counter-proposal is 0-based instead of 1-based. For example:

|- ( <" A , B , C , D "> ` 3 ) = ( _I ` D )
|- ( ( F = <" A , B , C , D "> /\ C e. V /\ D e. V ) -> ( ( F ` 2 ) x. ( F ` 3 ) ) = ( C x. D ) )

Mario

[fl]

It is a function. In fact, it is a (Word`S).

In that case it's ok.

--
FL

[fl]

The additional commas are not necessarily a bad thing; especially if you get a long run of constants it can get very confusing, e.g.

String 4 1 <_ 4 2

Pathological cases musn't be taken into consideration. The main idea is to have the possibility to right very
short strings like "¤ 5 (c phc /\c psc )c" . Everything else will be longer.
 
--
FL

[Mario Carneiro]

Actually, the real danger is when the constant expressions are long, and I can think of several use-cases where the individual entries of the string are not simply constants like /\c or 2. For example, take a look at konigsberg, where I have a need for a string of unordered pairs and build an ad-hoc mechanism for handling this in the proof.

As the constant expressions become longer, *especially* if the lengths vary, it can become difficult to tell where one constant ends and another begins. Another pathological case is String 3 U_ x e. String 5 A B C D E F G H. Humans aren't great at reading RPN notation.

Mario

[Mario Carneiro]

By the way, the commas are actually optional. <" A B C "> is also an unambiguous scheme for strings. (It is important that the begin and end sentinels are different; " A B C " would not work because of ambiguity in " " A " B " C " ", which could be either <" <" A <" B "> C "> "> or <" <" A "> B <" C "> ">.) The point about difficulty of reading heterogeneous undelimited lists of classes still stands, though.

Mario

[Norman Megill]

On 2/25/16 7:01 AM, 'fl' via Metamath wrote:

...

> You might also use predicates to express a String.
>
> String 4 RR CC + Intvl = { <. 1 , RR >. , <. 2 , CC >. , <. 3 , + >. }
> u. { <. 4 , Intvl >. }

If you are considering this as a way to define structures, our practice
has been to represent the indices using defined constants like ( Base `
ndx ), ( +g ` ndx ), etc. instead of fixed integers. While this makes
the initial definition more verbose, it gives us the flexibility to have
gaps and rearrange components without impacting later theorems.

The ndx function allows us to refer to structure components and defined
components identically. For example some authors define lattices with
ordering as primitive and meet/join defined, whereas others have
meet/join primitive and ordering defined. We can switch from one
definition to the other without affecting later theorems.

Norm

[fl]

If you are considering this as a way to define structures,

No I'm considering this to define strings in logics for instance or to pass parameters
to a function.

--
FL

[fl]

> By the way, the commas are actually optional. <" A B C "> is also an unambiguous scheme for strings.

In that case it fits my needs.

--
FL

[Mario Carneiro]

I just pushed a commit a7935db which defines string literals of length up to 8. Example theorems:


  df-s2 $a |- <" A B "> = ( <" A "> concat <" B "> ) $.
  df-s3 $a |- <" A B C "> = ( <" A B "> concat <" C "> ) $.
  df-s8 $a |- <" A B C D E F G H "> = ( <" A B C D E F G "> concat <" H "> ) $.

  ${
    s2eqd.1 $e |- ( ph -> A = N ) $.
    s2eqd.2 $e |- ( ph -> B = O ) $.
    s3eqd.3 $e |- ( ph -> C = P ) $.
    s3eqd $p |- ( ph -> <" A B C "> = <" N O P "> ) $= ... $
  $}

  ${
    s2cld.1 $e |- ( ph -> A e. X ) $.
    s2cld.2 $e |- ( ph -> B e. X ) $.
    s3cld.3 $e |- ( ph -> C e. X ) $.
    s3cld $p |- ( ph -> <" A B C "> e. Word X ) $= ... $.
  $}
.
  s3cli $p |- <" A B C "> e. Word _V $=
  s2fv1 $p |- ( B e. V -> ( <" A B "> ` 1 ) = B ) $=
  s5len $p |- ( # ` <" A B C D E "> ) = 5 $=
  s4s2 $p |- <" A B C D E F "> = ( <" A B C D "> concat <" E F "> ) $=

The Word definition has also changed from ( Word ` S ) to Word S, so that we can use the set Word _V of all strings on any alphabet. This change affected free monoids and free groups, konigsberg, as well as permutation signs in Stefan's mathbox.

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 metamath+u...@googlegroups.com.
To post to this group, send email to meta...@googlegroups.com.
Visit this group at https://groups.google.com/group/metamath.
For more options, visit https://groups.google.com/d/optout.

[fl]

Hi Mario,

> I just pushed a commit a7935db which defines string literals of length up to 8.

Thank you.

 
> df-s2 $a |- <" A B "> = ( <" A "> concat <" B "> ) $.

You should also replace concat by something short: +c or something like that so that we can write
unobstrusive strings like <" /\c phc  psc "> +c <" \/c "> +c <" /\c chc  thc "> (obviously with more that
three elements each time).

> [ Replacing ( Words ` X ) ]

No need in fact. As Norm says: if we take set theory seriously, only sets are needed.
I think he really wants that: few constructs with class variables and *only* sets.

The use of a construct with class variables in <" ... "> is only intended to have a natural and readable
representation not to have have actual parameters that would be proper classes.

--
FL

[Mario Carneiro]

On Mon, Feb 29, 2016 at 6:28 AM, 'fl' via Metamath <meta...@googlegroups.com> wrote:

Hi Mario,


> I just pushed a commit a7935db which defines string literals of length up to 8.

Thank you.

 
> df-s2 $a |- <" A B "> = ( <" A "> concat <" B "> ) $.

You should also replace concat by something short: +c or something like that so that we can write
unobstrusive strings like <" /\c phc  psc "> +c <" \/c "> +c <" /\c chc  thc "> (obviously with more that
three elements each time).

For one thing, +c is taken (cardinal addition). Also don't forget that it it a binary operation so needs parentheses, which probably affect the readability of long concatenated strings more than anything else.  But this is an easy thing to fix regardless of the decision, and I'd like to hear what others think. For my part, I would like to see more applications before committing to an "optimized" notation for strings, since they are only used a few times currently and they handle the existing tasks fairly well already. Note that "concat" is actually more commonly seen with variable strings than simply concatenating literals, since we have a notation for that now.

I assume you are talking here about very long literals (longer than 8), which will need "concat", but I question whether you will be able to make use of such a long literal in a theorem. Representation is one thing, but without theorems for manipulation it's not that helpful to have the string in the first place. konigsberg uses a string of length 7; how long of an actual string literal do you think you need? ("Unbounded" is not an answer.)

By the way, since this is a very short way of combining data, it is actually useful for a whole range of things beyond just strings. For instance, ran <" A B C D E "> is shorter than ( { A , B , C } u. { D , E } ) (provided that all the arguments are sets, the behavior on proper classes is different), and it is possible to write a coercion from <" A B C D E "> to <. <. <. <. A , B >. , C >. , D >. , E >. if that sort of thing becomes useful. ( G gsum <" A B C D E "> ) is shorter than ( ( ( ( A .+ B ) .+ C ) .+ D ) .+ E ), and it can also be written with seq as ( seq 0 ( .+ , <" A B C D E "> ) ` 4 ) if a group structure is not available.

> [ Replacing ( Words ` X ) ]

No need in fact. As Norm says: if we take set theory seriously, only sets are needed.
I think he really wants that: few constructs with class variables and *only* sets.

The use of a construct with class variables in <" ... "> is only intended to have a natural and readable
representation not to have have actual parameters that would be proper classes.

Sure, the thing about (Word`S) is not really related to the addition of literals, it was simply encouraged by it because <" A B C "> e. Word _V unconditionally, and a similar statement is not possible with (Word`S). It simplifies a lot of string theorems, eliminating all sethood hypotheses for S except for theorems like ( S e. _V <-> Word S e. _V ).

As for proper classes in <" ... ">, I set it up so that <" A "> = <" ( _I ` A ) ">, which seems to yield the best behavior. Using { <. 0 , A >. } directly causes <" A B C">. to not be a function or have holes in its domain if one of the arguments is a proper class.

Mario

[fl]

> It simplifies a lot of string theorems, eliminating all sethood hypotheses for S except for theorems like
> ( S e. _V <-> Word S e. _V ).

Yes but it weakens the set-theoretic prophylactic wall. It is not a good thing. And we are accustomed to check our
parameters in so many cases that we can do that once more.
 

As for proper classes in <" ... ">, I set it up so that <" A "> = <" ( _I ` A ) ">, which seems to yield the best behavior. Using { <. 0 , A >. } directly causes <" A B C">. to not be a function or have holes in its domain if one of the arguments is a proper class.

Don't use proper classes that's all. If everything is a set, you don't need to.

--
FL

[Mario Carneiro]

On Mon, Feb 29, 2016 at 12:45 PM, 'fl' via Metamath <meta...@googlegroups.com> wrote:

> It simplifies a lot of string theorems, eliminating all sethood hypotheses for S except for theorems like
> ( S e. _V <-> Word S e. _V ).

Yes but it weakens the set-theoretic prophylactic wall. It is not a good thing. And we are accustomed to check our
parameters in so many cases that we can do that once more.

For Word S, there is a good reason to have S as a proper class, and the restriction to sets is entirely unnecessary. For example, suppose the definition were only stated for subsets of the reals. Under the assumption S C_ RR, all of the theorems go through, but one has to ask if the restriction is necessary, or serves a purpose. If all of the theorems still hold on a larger domain, unchanged except for losing the restriction, then there is really no reason not to extend the definition to the widest "natural" choice. And again, under the old definition there was no easy way to refer to the proper class now called "Word _V", much less use it in string theorems where (Word`S) is expected.

As for proper classes in <" ... ">, I set it up so that <" A "> = <" ( _I ` A ) ">, which seems to yield the best behavior. Using { <. 0 , A >. } directly causes <" A B C">. to not be a function or have holes in its domain if one of the arguments is a proper class.

Don't use proper classes that's all. If everything is a set, you don't need to.

It's not about whether you are actually going to use it on a proper class. With a well-crafted definition, that "gracefully degrades" outside the desired domain, many theorems will hold on the wider domain, making them easier to use. Which theorem would you prefer to use:

$p |- ( # ` <" A B C D E "> ) = 5

or

$e |- ( ph -> A e. X )

$e |- ( ph -> B e. X )

$e |- ( ph -> C e. X )

$e |- ( ph -> D e. X )
$e |- ( ph -> E e. X )
$p |- ( ph -> ( # ` <" A B C D E "> ) = 5 )

?

Probably you will have all the prerequisites for the second theorem anyway, but to discharge them is twice as much work as letting the type inference for classes handle the hard work in the first option. (And when I say "work", I mean bytes of the output proof, as well as extra brain cells applied by the theorem author.) Imagine what it would be like if fvex only applied in the domain of the function. It's the same idea.

Mario