Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
I am not sure if this is an example of what I imagined would go under “nondeterministic computation”. Do you have a reference for people speaking this way?
Of course! It’s in the introduction of the review paper of Ehrhard on differential linear logic for instance. I’m gonna put references then.
Thanks for the reference. I see, this seems (will need to read more carefully) to be talking about what in the semantics should be direct sums of terms (“formal sums” in Erhard’s text), namely linear disjunction ( i have added that hyperlink to your paragraph).
If that is the case, then this is not so far from the notion of indefiniteness exhibited by the reader monad which my link in the sketchy hint-line in the Idea-section is alluding to: It would be exactly the kind of indefiniteness exhibited by the linear reader monad.
Except that the reader monad, via its monad operations, allows to actually keep track of the direct summands in the direct sum, which seems to be necessary to really speak of indeterminism (since it allows to “measure” a non-deterministic result to determine what it comes out to be in a given possible world).
In contrast, regarding a proof of the form “” of the bare type (i.e. without regarding its -algebra structure) as “non-deterministic” is just like regarding a classical proof of of the form “” as non-deterministic, which is not really the way one speaks (instead such a proof could be called redundant).
Thanks for all this.
I admit that I don’t see how this addresses my complaint, but maybe that wasn’t your goal.
Allow me to ask:
Is there an operational semantics of these formal sums of proofs in which either one or the other summand is picked up, non-deterministically?
Is there even a language structure to extract the two summands once they have been summed?
My (admittedly completely cursory) understanding so far is that the answer to these questions is “No”, because the sum happens, semantically, in some commutative monoid, and that’s it, then.
But if the answer to these questions is indeed “No”, then I’d be inclined to find that, interesting as the effect may be, it’s not about non-determinism.
Your questions are a little above my head, that’s why I just tried to better explain what I’ve already written.
You’re probably right, the answers must be no. I quote a paragraph of the introduction of the paper The differential lambda-calculus by Ehrhard, Regnier:
“Sums vs. non-determinism.
Notice that in our axiomatization of sums in the differential lambda-calculus, the non-deterministic reduction rule s+s′ → s will not be valid, but sums will nevertheless intuitively correspond to a version of non-deterministic choice where all the actual choice operations are postponed: the result of a term reduction will in general be a large formal sum of terms, and we can reduce the really“non- deterministic” part of the computation to a unique ultimate step consisting in choosing one term of that sum.This step is however a fiction and will not appear as a reduction rule of our calculus as otherwise essential properties such as confluence would obviously be lost. Another good reason for not considering this rule as an ordinary reduction rule is that, as suggested by the discussion above, it can be performed only when the “redex” stands in linear position. Note that, from a logical viewpoint, introducing sums is not at all innocuous. In particular, as it is well known in category theory, it leads to the identification between finite categorical products and coproducts, the and connectives of linear logic.”
However, the differential -calculus has been used in relation to the semantics of probabilistic programming language. Maybe would it correspond more to the kind of non determinism you’re looking for.
You should be able to find information about this in this report by Christine Tasson : Models of Distributed, Differential and Probabilistic Computation
Abstract:
“Since the 60s, semantics have proved most useful to introduce high-level languages allowing complex programs to be written and at an accurate mathematical level to be understood. In the 80s, linear logic was introduced by Girard following semantical properties reflecting resource usage in computation. This line of research was carried on by Ehrhard in the 2000s with the introduction of differential λ- calculus. In its models, programs are approximated by polynomials whose monomials represent queries to inputs along computation. This analytic approach has been a key tool to study quantitative properties of programs such as probabilistic computation. In parallel, since the 90’s, several geometric models was developed to give account to execution traces in distributed systems. In this habilitation thesis, we present models that we have studied in three distinct areas: distributed systems, differential lambda calculus, probabilistic programing, as well as general techniques to do so and the results they have allowed us to obtain. Those have required the use and the development of tools coming from combinatorics, directed topology, functional analysis, category theory and probability.”
I don’t know if it’s helpful but in case I mention it.
Is probabilist computation closer to what you mean by nondeterministic? Maybe it’s completely different, I don’t know well the subject.
And I admit that I’ve never well understood what means a non deterministic program concretely. For instance, I had lectures on nondeterministic automata and the nondeterminism was a little bit abstract to me. I don’t understand how such an automaton would work in the physical world.
Thanks for the quote in #9, that seems to settle the issue, to the negative. I have added that quote to the entry, and I have pre-fixed your not-quite-example by a cautionary line (now here).
Will add a tad of content to the entry now. I guess it’s my fault to leave a stub entry sitting around unattended.
I have now added some content to the entry.
a bare minimum of an Idea section (here)
a section on formalization via the reader monad (here)
a section with pointers to quantum computation (here)
I also tried to add more references on “nondeterministic turing machines” etc. but while I easily find many lecture notes on this, I didn’t find a good textbook yet. If anyone has more pointers, please be invited to add them.
Corrected: “Cut elimination-rule” -> “Cut elimination procedure”. The cut elimination is never an inference rule (it is not the cut rule) but a process on proofs of the system which is “one meta-level above the level of proofs”. See the section “Cut elimination as a computation” in the entry cut rule.
1 to 15 of 15