New answers tagged

0

The problem is equivalent to online knapsack problem. Let $n$ represents the number of items. Let the knapsack has capacity $B$. Every item $i$, has value $v_i=1$ and weight $w_i=p_i$. The offline optimal solution: Sort the items in increasing order of their weights ($p_{\sigma(1)}\leq p_{\sigma(2)}\leq \cdots \leq p_{\sigma(n)}$ for some permutation $\...


6

The standard well-formed-related predicate can be relatively easily extended to handle untyped PHOAS. The main subtlety is how to handle reduction at the type level. Here's a start of a two-place relation for well-typed in Coq: Require Import Coq.Lists.List. Reserved Infix "@" (left associativity, at level 11). Local Open Scope list_scope. Inductive expr ...


Top 50 recent answers are included