Three Dollar Quill

Okay, let's see.

Delimited summation notation has a lower and upper bound on an integer, and a function from an integer to a real.

Generalized summation notation has an iset (should there be something separate for specifically a set?) of some type T, and a function from T to real.

It may be pleasant to include a form that combines bounds with predicates, but I'm not sure how many "nice-to-haves" there are to lay out. Like, a single integer index, with lower and upper bounds, plus a predicate, seems sensible.

Then I read a little further, and remember some things that make it not clear to me how things should proceed. Like, working in Python-style pseudocode because I don't want to look stuff up, suppose we have Sigma(a, p), and I want to change it to Sigma(lambda k: a(k + 1), lambda k: p(k + 1))... That looks vaguely reasonable, although for the actual code I'll probably want something like a shift operator for this specific case?

The sense I'm getting is that this should be a "sandwich" type of thing, where the "boundaries" prefer simple delimited summation to delimited summation with a predicate, to summation with a predicate or iset or something.

Now, the chapter is discussing Iverson brackets, which I want to represent as a function from bool to a function from real to real.

Moving right along, I suppose the second function there would ideally have a default value of 1.0.

Although, maybe it's not a function, because we see also the possibility of "summation with no explicit predicates, but a bunch of Iverson brackets in the summand". How all of that gets represented depends on how much Dafny can "look inside" functions to pull stuff out. I'll have to experiment with that later. For now, let's assume it can, and try to contrive a situation where it's obvious if that's wrong.

Anyway, I got distracted and it's late. Better get to bed.

Good night.