I'm not sure if this is exactly the same but it reminds me a lot of recursive types and checking if two such recursive types are equal (see https://en.wikipedia.org/wiki/Recursive_data_type#Equirecursive_types). I looked into that a few years ago and it seems to be decidable with a relatively easy algorithm: http://lucacardelli.name/Papers/SRT.pdf (the paper is a bit longer but it also shows algorithms for subtyping)
To map this onto your expression problem maybe one can just take expression symbols as "type terminals" and use the same algorithm.
So these ‘moral’ intuitions
The sentence seems to be cut off in the middle
The law, as generally formulated, states that entropy increases with time. But how do we know that this is a physical law and not a pattern we notice and successfully extrapolate, in keeping with the main thesis under consideration?
I've recently read The Big Picture and spent some time chasing Quantum Mechanics Wikipedia articles. From what stuck, thermodynamics itself is an effective field theory of the Standard Model of particle physics. It is a macroscopic, consistent approximation of our current best QM theory. Part of this approximation is that ent...
I think some clarity for "minimal", "optimization", "hard", and "different conditions" would help.
I'll take your problem "definition" using a distribution D, a reward function R, and some circuit C and and Expectation E over R(x, C(x)).
Do we want the minimal C that maximizes E? Or do we want the minimal C that satisfies E > 0? These are not necessarily equivalent because max(E) might be non-computable while E > 0 not. Simple example would be: R(x, C(x)) is the number of 1s that the Turing Machine wi
Decidability of equivalence is broken somewhere between simply typed lambda calculus and System-F. Without recursive types you are strongly normalizing and thus "trivially" decidable. However, just adding recursive types does not break decidability (e.g. see http://www.di.unito.it/~felice/pdf/ictcs.pdf). Similarly, just adding some higher-order functions or parametric polymorphism does also not necessarily break decidability (e.g. see Hindley-Milner). In my (admittedly limited) experience, when making a type system stronger, it is usually some strange, som
... (read more)