[practal]

Yes and no. Yes, predicates are more flexible, because they can range over the entire mathematical universe, as they do for example in (one-sorted) first-order logic. No, names are not a problem, predicates can have names, too.

[agumonkey]

so if names are not an issue, the problem with the usual static type systems is that they lack a way to manipulate / recombine user defined types to avoid expressive dead ends ?

[practal]

What is the type of x / y, for x : ℝ and y : ℝ?

[magicalhippo]

What is the type of x and y? If it's ℝ, why wouldn't x / y be of type *ℝ (hyperreals)?

I'm just your average programmer, not into abstract logic stuff, but got curious.

[hansvm]

The hyperreals don't fix the x/0 or 0/0 problems. Infinitesimals have a well-defined division and take the place of a lot of uses of 0 in the reals, but the hyperreals still have a 0, and the same problem posed in their comment exists when you consider division on the hyperreals as well.

I'm also curious what they intended, but there aren't many options:

1. The question is ill-posed. The input types are too broad.

2. You must extend ℝ with at least one additional point representing the result. Every choice is bad for a number of reasons (e.g., you no longer have multiplicative inverses and might not even have well-defined addition or subtraction on the resulting set). Some are easier to work with than others. A dedicated `undefined` value is usually easy enough to work with, though sometimes a single "infinity" isn't terrible (if you consider negative infinities it gets more terrible).

3. You arbitrarily choose some real-valued result. Basically every theorem or application considering division now doesn't have to special-case zero (because x/0 is defined) but still has to special-case zero (because every choice is wrong for most use cases), leading to no real improvements.

[magicalhippo]

Good point, forgot about 0/0.

[agumonkey]

I'm tempted to say ℝ but it seems too obvious

[bmacho]

I would say ℝ u {undefined}

[agumonkey]

undefined because x / 0 ? ℝ includes infinity

[hansvm]

It's undefined because there isn't an obvious choice:

- At x:=0, every real is a reasonable limit for some path through the euclidean plane to (0,0). Ignore the 0/0 problem, then x/0 still has either positive or negative infinity as reasonable choices. Suppose you choose a different extension like only having a single point at infinity; then you give up other properties like being able to add and subtract all members of the set you're considering.

- However you define x/0, it still doesn't work as a multiplicative inverse for arbitrary x.

A good question to ask is why you want to compute x/0 in the first place. It is, e.g., sometimes true that doing so allows you to compute results arithmetically and ignore intermediate infinities. Doing so is usually dangerous though, since your intuition no longer lines up with the actual properties of the system, and most techniques you might want to apply are no longer valid. Certain definitions are more amenable to being situationally useful (like the one-point compactification of the reals), but without a goal in mind the definition you choose is unlikely to be any better than either treating division as a non-total function (not actually defined on all of ℝ), or, equivalently, considering its output to be ℝ extended with {undefined}.

Not that it directly applies to your question, ℝ typically does not include infinity. ℝ⁺ is one symbol sometimes used for representing the reals with two infinities, though notation varies both for that and the one-point compactification.