von Neumann entropy in simple type theory

[Lawrence Paulson]

As a general rule, this sort of question is analogous to questions often asked in disputes about programming languages: can algorithm A really be implemented in language L? And the answer is always yes, because language L is Turing-complete. But what we really want to know is how the implementation of A in L compares with its implementation in some other language L' with regard to various criteria such as elegance, performance, etc.

Still speaking generally (because I'm not familiar with some of the technicalities of the example), the only reason an implementation in simple type theory would be inconvenient would be because of a preference to formalise some entity, such as the N-th tensor power of P and E(P^N), as a type. There is however no reason why types need to play this role. It's worth recalling that types were introduced by Russell for the sole purpose of preventing paradoxes and not to take a central role as an abstraction mechanism.

Thinking now more specifically of HOL Light, a great deal of analysis is developed concretely over the domain R^N, where N isn't actually an integer but can play the role of an integer through a clever use of type schemes. So in particular, many results about topological spaces are proved for the case of R^N. This does not give us a development of abstract topology theory, and so HOL Light includes a separate formalisation of the notion of topological space where the carrier can be an arbitrary set (within simple type theory).

The introduction of type classes in Isabelle/HOL lets us develop some results about topological spaces in a somewhat more abstract form, but still with the very strong restriction that a topological space must be a type; a more general development topology theory (exactly like the HOL Light one) is still necessary in order to lift that restriction.

Larry Paulson
On 29 Feb 2020, 01:11 +0000, José Manuel Rodríguez Caballero <josephcmac at gmail.com>, wrote:
> Dear FOM members,
>    For the researchers who are interested in developing mathematics in simple type theory rather than in ZFC, to express the following theorem (Ref 1. page 16) in the language of simple type theory may be rather challenging:
>
> Theorem A. Let S be a complex Hilbert space. Let P be a density operator defined on S and let T be a closed subspace of S; we define P(T), called the P-mass of T, as the sum of P(t), where t runs through an orthonormal basis of T (this definition is independent of the chosen basis). Let E(P) be the infimum of the logarithm of the dimension of T, where T runs through the subspaces of T such that P(T) is greater than one half of P(S). Then, the sequence E(P^N) / N, indexed by N, converges, where P^N is the N-th tensor power of P and E(P^N) is taken with respect to the Hilbert space S^N (N-th tensor power of S).
>
> By the way, the limit in Theorem A is called the von Neumann entropy of P (Ref. 2).
>
> I would like to ask two complementary questions:
> 1. Is there a way to express Theorem A in a simple type theory?
> 2. If the answer to question 1 is negative, how could it be proved that this theorem cannot be expressed in simple type theory?
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20200302/d1ca5f2e/attachment.html>