The function that maps a set to its cardinality is actually a measure on *some collections of sets that satisfy certain axioms. Those axioms being it's closed under set union and set minus (intersection follows as a theorem from these two). Usually we desire countable unions, which is fine on a collection of finite sets because countable unions of finite sets is just a finite union**. So in a sense your language already meets the axioms. You could define other measures, in a sense giving more "weight" to some set. We just established that it does have an additive set function, thus we have a measure of your sets, the "cardinality-measure" for lack of a better term. Which means there's probably others.



Ah, gotcha. I guess this stuff is for the academics.

*as long as infinity = infinity for all infinity

**as long as the union of all sets in the collection is finite

The second part of Jon's post looks interesting and I look forward to reading it, but let me respond to this:



I am sure you are right about this and from what I understand, I agree with the sentiment too.

But what I mostly meant was that Reid's suggestion that we "define an additive set function and turn the space of tables into a measure space" reminded me of the flavor of very old writings of mathematicians from the 40's and '50's, before the right mathematical abstractions for computer science were obvious enough that one could define crazy things like this willy-nilly and expect a positive probability that they'd at all be useful.

Like, there's a very old paper by Kleene, where he invents regular expressions, but the paper was about neural nets.

Edit: "define", not "definitely"

I will keep this in mind, since I had planned to look into TLA+, which I have heard good things about.

Actually, this same fellow Ron Pressler seems to have just spoken to this matter in his third installment of his TLA+ series of blog posts:



So the tl;dr for me, if I understand this properly, is that TLA+ can very well be a vehicle for model checking used in a way that heeds Jon's advice to enforce the correctness of the specifications themselves, since TLA+ makes no distinction between type and program anyway.

Hey, I never said it would be useful, just that it would be cool. It does seem like Jon stumbled upon measure theory a bit though.

As for the uses, you could probably define measures that let you do cool things with the language beyond just taking the cardinality of a set. Extend its uses. For instance, probabilties, and so forth. Though I don't know how that'd look on the computer science end of things.

Also, I think you could probably get integration out of it.

What's more interesting to me than measure theory is topology. Wikipedia tells us that "each Boolean algebra B has an associated topological space, denoted here S(B), called its Stone space".

And if you follow the thread between topology and types far enough, you can get to wild things using category theory and topoi, or even algebraic topology, where you have people like Vladimir Voevodsky and his work in Homotopy Type Theory and Univalent Foundations:



But I can see how adding mathematical information to a programming language would be useful to mathematicians who already use said formalism (in your case, measure theory).

Wait, isn't Kolmogorov complexity still an important topic in CS? I mean, I'm not well-versed in 1950's CS articles, so I guess only the useful was taken out?

I would actually hazard to guess that Kolmogorov complexity is more useful in applications of computer science, especially to complex systems theory.

Also, Kolmogorov introduced it roughly half a century ago, which is not exactly recent. But like I said, people like Wolfram are still at at and it is certainly a hot topic to try to expand the purview of C.S. It's just that the basics of the theory have been around long enough (and measure theory even longer), that I would have expected the sort of thing you dreamed up to have been discovered by now (and maybe it has been).

But to be fair, I see that you are right about it being fundamental, even if it was discovered a bit later than the earliest stuff. From Wikipedia:

(It looks like I was pretty wrong when I guessed about Komogorov complexity being used mostly outside C.S. itself, seeing that the Wikipedia article is chock full of applications within C.S.)

I don't know much about Boolean algebra, though I proved some stuff about Boolean rings yea months ago. I've brain rotted out of topology though. At this point I want to get back in. I'll probably have to get a copy of a text on smooth manifolds soon and do differential topology.

But the question you should be asking about Stone spaces is what they are useful for.



Well, proving that it's a measure space wouldn't be useful to just mathematicians, measure theory is a well-developed field, and you can pull quite a bit out of the theory.

I would expect someone much cleverer than me has done quite a bit of programming related to measure theory, so yeah, I just got excited because he basically said his statements were a sigma-ring.

Actually, Reid, for overlap between probability theory and programming, you can check out probabilistic programming. It's full of theoretical connections to machine learning, prolog, or statistical relational learning (which is somewhere in between the first two).

Quite a bit, if you are interested in algebraic approaches to formal methods.

To the presume the same about measure theory will most likely imply a probabilistic programming model (follow the link in my post above), although I admit there could be other applications.

Just be careful, though. Richard Hamming once said:

...and I think you and I have just lost the interest of literally everyone else in this forum.

oooph.

ani lo yodea eykh ledaber anglit

bo shuda... my pee kasa Grismath. dolpee kikyuna! ohhhhhh

UTTINI

[RIGHT]?אבל למשעה אתה מדבר עברית? אתה גר בארץ[/RIGHT]

I am the humanities version of this (though the degree I am working on is 'science') and I mostly tell anecdotes about Diogenes (and Feynman actually soooooo) so I guess I am involved with greek life lolololol. But no, you will not find me at frat parties. Theatre department parties and drag shows definitely yes though.



Yes but some (some) of their slaves were treated better than the way we treat our slaves now for example. I'm not one for golden age thinking in either direction, but while in general things are better I can't really get with the 'it is a better time to be alive than ever in every way be grateful and don't criticize anything' that the techno optimists and priests of progress seem to think I have to believe to not be a dirt eating moron.

I'm definitely not advocating we don't complain today, I mean I'm a pretty big whiner about the state of things myself. But I think it's clear from reading the texts that Greek society was still far more cruel than ours. We don't have so much literal slavery (?) proportionately but we do have a worldwide proletariat that's treated terribly. Maybe the Greek slaves were treated better than black slaves in America, probably so in fact. So you have a point.

The thing with pharmakos sacrifice is that it's something of an incomparable event. I maybe left out too many details. For one, the entire town would be forced, literally, to participate so that nobody could build sympathy with the victim. It's like a serious, adult version of muckle. I don't see anything comparable to that in modern society.

Also, I think the Greek word sophrosyne needs to re-enter our vocabulary. And all people need a bit more of it.

אם אתם רוצים לדבר על עבדות בבקשה בשפות אחרות

הנושא הזה לא בשביל אנגלית

Yeah that was my general point re:slaves as the 1800s was like ten minutes ago in my mind. Though the general treatment of the global proletariat (which doesn't include anyone here, and can definitely be portrayed as 'slavery' without too many gymnastics) is definitely an unprecedented flavor (though perhaps not degree) of cruel, so I'm not sure where it actually ranks in the oppression olympics. Regardless, all of us including those greeks are prisoners in the black iron prison that corrals us into participating in things along these lines, to whatever extent we do.

I have not read very much about this weird greek kind of sacrifice, I will have to look into it more, thanks for telling me about it.

This thread does not deliver.

I thought it was going ok until the cliquish academic elitism stuff

the social sciences are for retards who don't understand statistics. ugh. but at least they aren't too autistic to understand math, like those rapey engineering students.

Ah, yeah, I think the main difference is westerners have a comedy of innocence trying to put distance between us and the cruelty of our economic system, we normally don't have to face it directly. But it's nonetheless there.



It's called pharmakos and there's a great journal article, "Scapegoat Rituals in Ancient Greece" by Jan Bremmer which gives it a good treatment.

Ironically pharmakos is pretty close to pharmakon, which means either "cure" "poison" or "purify", and is the word used to describe what happened to Socrates, some philosophers make a few nudge nudge suggestions but academics hate this.

They (we?) probably don't hate it as much they hate Derrida.

^ also there's little "normal" in any Greek sacrifice.. even the normal versions are pretty weird by our standards



Lol my mistake. Reverend Jones and I are to blame for the math talk.



Uh...

That's probably true.

Dutch
English
French
German
Spanish
Latin
Ancient Greek
(some) Japanese, studied it for one year, a long time ago. Most of it has sunk away in the mists of time.

You're right. Those comments I made were really ****ty. I'm sorry about that.

It's not just you

I know, I did my part in saying/normalizing the activity though.

The S.F. knows I've said my share of ****ty things on this board. On the other hand, I don't like to emphasize the penance aspect of rectifying these sins, because while saying privilagy stuff that scapegoats some outgroup makes us all cringe, I've always felt that the potential for negative social consequences that this kind of darkness revealed within ourselves could engender--if we don't put a mirror up to it (which we absolutely ought to do!) before we let ourselves do real harm down the road-- is in some ways secondary to another problem.

Namely, that explaining away something neutral to negative about ourselves by scapegoating an outgroup is lazy, and more importantly, usually flat out wrong.

This board could be different, but I imagine that only 1% or less of people called autistic are actually autistic at all. And while it's a ****ty thing to say--especially if it becomes normalized (stop to think about where the word "dumb" comes from)--the most damaging consequence of being this lazy is that that the actual problems you have go totally unacknowledged, just because it's amusing enough to indulge for a moment in a humorous fantasy that you in fact have a genetic and therefore immutable problem, which you can laugh at because it's a fantasy after all, and also use to hide your actual shortcomings, because genetics are immutable.

"He's pretty stupid." Oh, that's just because he's "dumb". Case closed.

"He's socially awkward." Easy, he's "autistic".

See, it makes you a dick, but more importantly, you are hurting yourself because you justify a lack of introspection hiding behind humor.

Which, I believe, is a pretty good description of 4chan, so perhaps this is a juncture to bannish the meme and cast it back from whence it came.

(I just scapegoated 4chan as a way of hiding my real problems. )