Can someone who knows a bit about constructivism and computational interpretation of logic tell me why call/cc doesn't suffice as a witness for double negation elimination? What’s not constructive about it?

@im it is not constructive because nondeterministic computation can be built with call/cc

Nondeterministic in what sense? In the sense that if you run the whole program multiple times it will do different things (seems like that ought to require some external input in principle), or just that the return value of a given function might not be the same in all contexts? I guess I can see why that's surprising but I don't understand what problems it could cause

@im It is nondeterministic in the sense that, if you know Scheme's "implementations are free to choose evaluation order", it is permissible for a Scheme evaluator to use a random number generator to pick evaluation order, or if you think using a RNG is ridiculous, it also means different implementations can give different result when running the same program. This is also known as "Church Rosser property cannot be maintained if introducing call/cc"

@ldbeth OH, saying Church-Rosser gave me what I needed to get it, I think. So the problem it causes is that once your expressions include control operators you can no longer reason syntactically by rewriting terms in whatever order is convenient, because different reduction orders might yield different values? You have to know in detail what the machine is actually doing. Or something like that.

@im To give computational interpretation to classical logic needs the notion of process. By simply adding call/cc to typed lambda calculus would make the system “unsound” as it breaks certain properties that are considered nice, in reality almost all typed programming languages can be used for practical purposes have unsound type system, but as a logic it needs to be flawless.

@ldbeth so to my understanding, when you branch on a call/cc-based witness for A∨(A→⊥), you initially take the negative branch. Then, if you later find across some A-term and feed it to this 'function', instead of returning an impossible value (or diverging, or whatever) it transports you to an alternate reality where you took the positive branch all along.

Is that about right? Just trying to understand this stuff better, I'm a dabbler at best

@ldbeth I guess what I'm interested in is whether this is a problem for things like totality checking and type-driven programming, i.e. do you necessarily introduce inconsistency in an otherwise-total language by incorporating classical operators like that

@im the simple answer for this is yes, call/cc also cause trouble to termination check (well there are much simpler functions cannot be proved to be terminating, such as the Collatz Conjecture). The longer answer is for computational interpretation of classical logic, it would be more like two players competing each other.

Sign in to participate in the conversation
Mastodon @ SDF

"I appreciate SDF but it's a general-purpose server and the name doesn't make it obvious that it's about art." - Eugen Rochko