Graph query semantic formalization #2
Conversation
CCFPQ/CCFPQ_Result.v
Outdated
| Definition getLabels VV AA xl1 xl2 (walk : D_walk VV AA xl1 xl2 VL AL) : list symbol := getLabels' AL. | ||
| Definition getLength VV AA xl1 xl2 (walk : D_walk VV AA xl1 xl2 VL AL) : nat := getLength' AL. | ||
|
|
||
| Record CFPQ_Relational_query_result : Type := { |
There was a problem hiding this comment.
Не нашёл ничего про связь ответа с языком, заданным грамматикой.
CCFPQ/CCFPQ_Result.v
Outdated
| }. | ||
|
|
||
| Record CFPQ_All_path_query_result : Type := { | ||
| g'' : grammar; |
There was a problem hiding this comment.
Возрастающее кол-во штрихов не улучшает читабельность кода.
CCFPQ/CCFPQ.v
Outdated
| @@ -31,10 +34,10 @@ Section CCFPQ. | |||
|
|
|||
| Inductive CCFPQ_Builder : V_set -> Nat_set -> list var_EitherVertexNat_pair -> Type := | |||
| | Empty_query : CCFPQ_Builder V_empty Nat_empty [] | |||
| | Add_free_var : forall (v : V_set) (n : Nat_set) (var_evnp_l : list var_EitherVertexNat_pair) | |||
| | Add_free_var : forall (v : V_set) (n : Nat_set) (var_evnp_l : list var_EitherVertexNat_pair) | |||
There was a problem hiding this comment.
Дайте, пожалуйста, нормальные имена всем сущьностям. Читать код с V_Set и прочим очень тяжело.
CCFPQ/CCFPQ_Result.v
Outdated
| Derivability_relation g V A x' x2 v2) -> | ||
| Derivability_relation g V A x1 x2 v. | ||
|
|
||
| Theorem Parse_tree_to_relation : forall (g : Grammar) (V : V_set) (A : A_set) |
There was a problem hiding this comment.
Сложно, слишком много "сторонних" параметров. В конечном итоге должно получиться утверждение про грамматику, граф и формулу. Всё остальное должно исчезнуть.
There was a problem hiding this comment.
То же самое про остальные теоремы, лемы и т.д.
There was a problem hiding this comment.
Все эти сущности используются в определениях, без них обойтись нельзя
There was a problem hiding this comment.
Странно, а в нормальных утверждениях их нету. Что-то тут не так. Есть просто граф и грамматика. Если что-то нужно ещё, значит надо это "прятать".
There was a problem hiding this comment.
Эта теорема показывает, что из дерева разбора можно построить отношение выводимости.
Определение из статьи:
В Тексте граф G = В коде граф это (V : Vertex_set) (A : Arc_set) - вершины и ребра
В Тексте грамматика С = В коде грамматика (g : Grammar)
В тексте вершины m n = В коде (x1 x2 : Vertex)
Параметризуемый стартовый нетерминал грамматики в тексте а = В коде (v : var).
Само утверждение теоремы: Parse_tree g V A x1 x2 v -> Derivability_relation g V A x1 x2 v
Из любого дерева разбора строим отношение
There was a problem hiding this comment.
Ну, вот хотя бы набор рёбер и вершин можно спрятать в один тип "граф". Это и читабельность повысит и снимет вопросы из разряда "вообще-то граф это не просто несвязанный набор вершин и рёбер. Как минимум, вершины часть инцедентны каким-то рёбрам".
#1