matzemathics

import Mathlib.Data.Finite.Defs
import Mathlib.Data.Finset.Fold

structure Variable where
  index: Nat
  deriving DecidableEq

theorem Variable.ext (v₁ v₂: Variable): v₁ = v₂ ↔ v₁.index = v₂.index := by
  constructor
  . intro; congr

matzemathics

Datalog type analysis

In this document I propose two symmetric algorithms, which can be used in conjunction for determining the minimal types of datalog predicates.

Nomenclature

A datalog rule takes takes the form

p(t1, .. tn) :- q1(s1, .. sn), ..

matzemathics

#include <stddef.h>
#include <stdlib.h>
#include <stdio.h>
#include <string.h>
#include <assert.h>

typedef struct fs_node fs_node;
typedef struct fs_list fs_list;

struct fs_list

matzemathics

/*
 * This Source Code Form is subject to the terms of the Mozilla Public
 * License, v. 2.0. If a copy of the MPL was not distributed with this
 * file, You can obtain one at https://mozilla.org/MPL/2.0/.
 */

/* author: Matthias Meißner (geige.matze@gmail.com) */

#include <stdio.h>
#include <stdlib.h>

matzemathics

#include <variant>
#include <vector>
#include <iterator>
#include <algorithm>
#include <type_traits>

#include <cassert>
#include <string>
#include <iostream>