TezlaOil
Imagine that 10 normal people and Bill Gates want to buy bottles of wine. Bill goes for a bottle of $6000 Richebourg Grand Cru, and the 10 normal people always go for Shitscreek Red, sold for $4. So about 9% of the buyers are willing to pay extra for the name brand.
After the Great Wine Tax Bill of 2021, the prices are both increased by a fixed per-bottle amount of $6000. So now the Richebourg costs $12000, and the Shitscreek costs $6004. The 10 normal people migrate to beer, and Bill Gates still buys Richebourg. So about 100% of the buyers are willing to pay extra for the name brand.
-- Jean-Yves Girard: Locus Solum
In Agda, you would type something like `nat-ind ?x ?y` into a hole of type (forall m -> P m). Then ?x becomes a hole of type (P zero) and ?y becomes a hole of type (forall n -> P n -> P (suc n)), and you can fill these holes with proofs at your own leisure. It does not feel all that different from using `induction m` in Coq. In Agda, you'd normally implement your "reflective tactics" as functions, or you'd write macros if you really need them (e.g. for ring solvers), but there is no separate tactic language and proofs are never tactic scripts.
It totally would. Statistically, a sample size of 282 out of a population of 60000 is pretty good.
If this test was authentic, we would be 95% sure that the true percentage of the population who think that the memo is harmless is between 47% and 60%.
For example, a 'random' tour of the traveling salesman might have a nice sensible path between Paris and Moscow, while another solution has a good path between San Francisco and Mexico City. Chromosomal crossover (the fundamental operation of genetic algorithms) can create "offspring" tours that contain both of these components.
This is not at all analogous to exploring the middle between two local optima - the solution space often has no meaningful geometric structure, so being located "between" two other solutions may not make sense at all.
Instead, genetic methods work well for various messy industrial engineering such as strip packaging design or antenna design. One of my favorite recent results solves a structural engineering problem using grammatical evolution [1].
[1] http://www.sciencedirect.com/science/article/pii/S0926580513...
[1] softwarefoundations.cis.upenn.edu/current/index.html