AIUI, up until Scott, λ-calculus had mathematicians saying "yes, it works in practice, but can it ever work in theory?": say we have a universe of discourse D, and we want, per λ-calculus, to have functions D->D (D->D->D, etc.) be part of this universe of discourse. If D is a windowless monad, with a single object, we're ok: there's only 1 arrow (1^1) from 1 object to 1 object, namely the identity, so we just go ahead and identify it with the object. However, as soon as we have two objects in D, we have a problem: there are 4 arrows (2^2) from 2 objects to 2 objects, so even if we attempt to identify objects and functions we don't have enough for all the functions, and the problem only gets worse (N^N) as we have N>2 objects.
Scott's contribution was to cut down the cardinality of the function space: by restricting it to continuous functions (ie only those functions that have finite approximations, which is to say they don't do anything strange "at infinity") one not only gets what most people would admit is a reasonable model of computation, but -calculus then works in theory, as D->D can now fit inside of D.
What I was trying to explore (and maybe the trouble with asking an LLM about this sort of thing is that they're unlikely to push back hard enough?) is the notion that even given an "angelic turing machine", one still couldn't compute in a way than an earthly turing machine couldn't simulate.
A first approach to programming with quantum effects is the quantum λ-calculus [SV09].
Nevertheless, that language does not handle quantum programming as an algebraic effect, since
it requires measurement into classical data to control the flow of execution.
pp23 1st para has more of the same
In the quantum
λ-calculus, a qubit has to be measured before influencing the control of a program. These
models are not of interest to this thesis, because the use of measurement breaks superposition,
therefore it does not preserve the aforementioned quantum effect.
[SV09] Peter Selinger and Benoit Valiron. Quantum lambda calculus. Semantic techniques in quantum computation, pages 135–172, 2009.
Keye Martin: be right back (I didn't see much there either.)
in my own heap: one might be able to use Scott continuity to replace lemma 7?
Pay attention to how the "control gates" (as in SV09) are invoked
pp7:
The crucial step in Shor’s algorithm, after the quantum Fourier transform, is to take a quantum measurement, with the property that the probability of observing a state that is close to an integral multiple of 2^n/ω
is high.
pp12 has this speculation
>At its most fundamental
level, it is not permitted to ask the computing machine to scan a continuously deformed symbol
from ξ to ζ, while a mathematical homotopy can easily be envisioned.
Scott's contribution was to cut down the cardinality of the function space: by restricting it to continuous functions (ie only those functions that have finite approximations, which is to say they don't do anything strange "at infinity") one not only gets what most people would admit is a reasonable model of computation, but -calculus then works in theory, as D->D can now fit inside of D.
What I was trying to explore (and maybe the trouble with asking an LLM about this sort of thing is that they're unlikely to push back hard enough?) is the notion that even given an "angelic turing machine", one still couldn't compute in a way than an earthly turing machine couldn't simulate.
Does that make sense?