roconnor
/ MemoOrdBinTree.v
Created May 14, 2018
Memoization for structurally recursive funcitons over binary trees in Coq (with poor performance).
View MemoOrdBinTree.v
| Require Import Arith. | |
| Require Import Omega. | |
| Set Primitive Projections. | |
| Set Implicit Arguments. | |
| Inductive binTree : Set := | |
| | Leaf : binTree | |
| | Branch : binTree -> binTree -> binTree. |
roconnor
/ MemoBinTree.v
Last active May 14, 2018
Memo Trie for funcitons over binary trees in Coq (no support for memoizing structually recursive functions though)
View MemoBinTree.v
| (* In relation to https://cstheory.stackexchange.com/questions/40631/how-can-you-build-a-coinductive-memoization-table-for-recursive-functions-over-b *) | |
| Require Import Vectors.Vector. | |
| Import VectorNotations. | |
| Set Primitive Projections. | |
| Set Implicit Arguments. | |
| Inductive binTree : Set := | |
| | Leaf : binTree | |
| | Branch : binTree -> binTree -> binTree. |
roconnor
/ ExtendedIncompletenessInQ0
Last active Feb 21, 2016
View ExtendedIncompletenessInQ0
| // Define Computably Enumerable (aka recursively enumerable) predicates. | |
| CESet : (Nat -> o) -> o | |
| CESet := \p. exists f \in PRF2Set. p = (\n. exists m:Nat. 0 < f n m) | |
| // Standard Model | |
| interpT : (Nat -> Nat) -> Term -> Nat | |
| interpT := \v. TermR_(Nat) v 0 (\t. S) (\t. \s. \n, \m. n + m) (\t. \s. \n. \m. n * m) | |
| interpF : (Nat -> Nat) -> Formula -> o |
View PatriciaTrie.v
| Require Import Bvector. | |
| Require Import Eqdep_dec. | |
| Set Implicit Arguments. | |
| Unset Strict Implicit. | |
| Unset Printing Implicit Defensive. | |
| Definition bCompare (x y : bool) : comparison := | |
| match x, y with | |
| | false, false => Eq |