I hereby claim:
- I am kkostya on github.
- I am kostya_imandra (https://keybase.io/kostya_imandra) on keybase.
- I have a public key ASCUVV8FQdvjmwaYjg9M7DChJknkKWODHPKVNRGu1OrsgAo
To claim this, I am signing this object:
http://glslsandbox.com/e#32520.0 | |
#### Voronoi: | |
http://glslsandbox.com/e#526.0 | |
http://glslsandbox.com/e#552.1 | |
http://glslsandbox.com/e#31987.0 | |
#### Simple 3D | |
http://glslsandbox.com/e#55.0 | |
http://glslsandbox.com/e#125.0 |
I hereby claim:
To claim this, I am signing this object:
#include <functional> | |
class A {}; | |
class B {}; | |
typedef std::function<B(A)> F; | |
typedef std::function<B(F)> G; | |
typedef std::function<B(G)> H; | |
F proof(H h){ | |
auto t = [](A a){ |
pairwise = lambda b: zip(*((lambda a: (lambda x: (next(x[1]), x))((iter(a), iter(a))))(b)[1])) |
# Python3 implementation of Heap's algorithm | |
# https://en.wikipedia.org/wiki/Heap%27s_algorithm | |
def heap(lst, k=None): | |
if k is None: k = len(lst) | |
if k == 1: | |
yield(tuple(lst)) | |
return | |
yield from heap(lst, k - 1) | |
for i in range(k-1): | |
m = i if k % 2 == 0 else 0 |
let aStayStrategy = (door,choice) => | |
switch(door,choice){ | (DoorA,Stay) => 1.0 | _ => 0.0 }; | |
expected_reward( | |
make_scenario_pmf(pDoorsBiased,aStayStrategy) | |
); | |
let cSwapStrategy = (door,choice) => | |
switch(door,choice){ | (DoorC,Swap) => 1.0 | _ => 0.0 }; | |
expected_reward( | |
make_scenario_pmf(pDoorsBiased,cSwapStrategy) | |
); |
instance ( (strategy) => Real.({ | |
valid_strategy(strategy) && | |
( expected_reward ( | |
make_scenario_pmf(pDoorsEqual,strategy) | |
) == 2000000.0 / 3.0 ) | |
})) |
verify ( (strategy) => Real.({ | |
valid_strategy(strategy) ==> | |
( expected_reward ( | |
make_scenario_pmf(pDoorsBiased,strategy) | |
) <= 2000000.0 / 3.0 ) | |
})) |
verify ( (strategy) => Real.({ | |
valid_strategy(strategy) ==> | |
( expected_reward ( | |
make_scenario_pmf(pDoorsBiased,strategy) | |
) <= 800000.0 ) | |
})) |
verify ( (strategy) => Real.({ | |
valid_strategy(strategy) ==> | |
( expected_reward ( | |
make_scenario_pmf(pDoorsEqual,strategy) | |
) <= 1000000.0 / 3.0 ) | |
})) |