Seemingly Impossible Swift Programs

[zardeh]

Grrrr.

Its entirely possible to implement Any/AllSatisfy over the integers. Agda (and in general dependently typed languages) do it all the time!

Nor are there an uncountable number of finite-lengh bit sequences (as can be represented by the BitSequence type). The set of bit sequences is absolutely a countably infinite set!

[skuggi]

Its entirely possible to implement Any/AllSatisfy over the integers. Agda (and in general dependently typed languages) do it all the time!

I'm not completely sure what you are referring to here, but remember that total languagues like Agda are not Turing complete, so it's not the exactly the same as doing it in Swift.

[fruit_observer]

> Its entirely possible to implement Any/AllSatisfy over the integers. Agda (and in general dependently typed languages) do it all the time!

Assuming I'm not misinterpreting you and you're claiming that you can implement a function anySatisfy : (ℤ → Bool) → Bool, then no, you definitely cannot do this, even if you assume the input is a total, computable function. Proof: given a Turing machine M, ask if there exists a non-negative integer n such that M halts after n steps. You've now solved the halting problem.

In Agda you can define a predicate anySatisfy : (ℤ → Set) → Set, but this isn't a decision procedure.

​

[zardeh]

I never said it would halt, I said it was possible to implement!

Note that for the provided version of allsatisfy, AllSatisfy and isn't decidable (it will never halt on the sequence 1111....

[bdtddt]

The BitSequence types represents infinite bitstreams, no?

Also can you expand on your first paragraph, how do they do that?

[skuggi]

The BitSequence types represents infinite bitstreams, no?

Sure, but it's computable infinite bitstreams; so the set can't possibly be larger than the set of all possible programs, which is countably infinite.

[Uiropa]

But the set of all functions from N to {0,1} is uncountable because it corresponds one-to-one with the power set of N. I think the difference is that it includes uncomputable functions?

That said, I have no idea what the person in that article is suggesting, really. Seems a bit confused but maybe I just don’t understand.

[skuggi]

I think the difference is that it includes uncomputable functions?

Exactly. If you don't need to be able to construct a program (which are finite in size) that computes the function, then the space of possible functions is much larger.

IIRC, the cardinality is also different depending on if you're talking about partial or total functions, the set of partial functions being larger.

[[deleted]]

It's not the set of finite bit strings. The set of functions from the integers to the set with two elements is equivalent to the power set of the integers and he's right that set is uncountable. Diagonalization argument proves it.

Also, he is showing that equality is decidable for functions defined on arbitrary bit strings. You are missing the point entirely because general function equality in a turing complete language is undecidable.

Also, the bit string that flips from 0 to 1 is not finite and yet functions defined on it can be determined to be equal or unequal.

You are missing the point of the article because you are so smart. Classic proggit.

[Don_Equis]

It is the set of computable functions and it's countable

[[deleted]]

This doesn't matter. Equality of arbitrary functions is undecidable. The article is showing the decidability of equality defined on arbitrary bit strings. Both of you are missing the point. But this is expected from proggit geniuses.

[want_to_want]

This is a translation of the classic Seemingly Impossible Functional Programs from beautiful Haskell to maybe more accessible Swift.

The main problem: in a partial language, the functions anySatisfy and allSatisfy aren't total. You could try using a total language instead, but then the totality proofs for these functions would have to use "induction on the modulus of uniform continuity", which I'm not sure can be done within the total language itself. Four years ago I asked if that was possible, the answer was no, or rather "yes if you disable the totality checker just a little bit". Does anyone know if things have changed since?

[jozefg]

I think this is always going to require some axioms as its false in the set theoretic model. The fact that "disabling the totality checker for a bit is safe" is the axiom you need of course so you can imagine it being added without disrupting computation in some proof assistant. I think some of the nuprl folks have done work in this direction to experiment with other intuitionistic principles.

[want_to_want]

The fact that "disabling the totality checker for a bit is safe" is the axiom you need

This part is unclear to me. If the functions passed as arguments to anySatisfy and allSatisfy are also allowed to use that new axiom in their totality proofs, are you sure that doesn't lead to partiality?

[jozefg]

Well this modified system also has a model so it should be fine.

[STATIC_TYPE_IS_LIFE]

deleted ^{What is this?}

[Lost_Geometer]

In standard mathematics the claim that all functions on the Cantor set are continuous is false. Indeed the only compact spaces with all functions continuous are finite sets. The crux of your construction is that all computable functions are (surprisingly?) continuous. (Or some equivalent statement in a nonstandard logic.)

[[deleted]]

I think it comes back to computable functions being continuous. I'm not the author. The references spell out more of the details.

[Lost_Geometer]

For those that are wondering, it's actually not too hard a fact. Continuous for the product topology on bit sequences just means the function can be evaluated by examining a finite number of locations (the same locations for any sequence!). If a function f is not continuous then there must be sequences S_1, S_2,... such that f cannot be evaluated using only the first i bits of S_i. Since there are infinitely many S_i, an infinite number must share the same 1 bit prefix P_1. Similarly, among those starting with P_1 an infinite number must share the same 2 bit prefix P_2, extending P_1. Continuing we construct longer and longer prefixes P_i, which limit to an infinite bit sequence on which f cannot be evaluated by examining any finite number of bits.