rvanbruggen

Graphs are everywhere - also in Religious Texts

This is going to be an interesting and in some ways even fascinating blogpost. I have thoroughly enjoyed researching it and playing around with the latest and greates Neo4j tools while doing so, but I must say that it's also one of the first blogposts that I can remember where I am a bit uneasy about the content. Why? Because it's about, or at least in some ways touches, religion.

First let's start with some background here. Some things that you should know about me:

• I was born and raised in Belgium, which is - or at least was - a predominantly Catholic Christian country. There's churches and chapels on every corner of the street here.
• My parents were/are far from religious, never took me to church, but did give me many of the Catholic Christian values - and these were engrained in me even more clearly because of my 13 ears in Jesuit schools in Antwerp and Turnhout.
• as an adult, I became increasingly distantiated from all rel

andrejbauer

(** An attempt to formalize graphs. *)

Require Import Arith.

(** In order to avoid the intricacies of constructive mathematics,
    we consider finite simple graphs whose sets of vertices are
    natural numbers 0, 1, , ..., n-1 and the edges form a decidable
    relation.  *)

(** We shall work a lot with statements of the form

tomconte

const fs = require('fs');
const solc = require('solc');
const Web3 = require('web3');

// Connect to local Ethereum node
const web3 = new Web3(new Web3.providers.HttpProvider("http://localhost:8545"));

// Compile the source code
const input = fs.readFileSync('Token.sol');
const output = solc.compile(input.toString(), 1);

andrejbauer

(* How do to topology in Coq if you are secretly an HOL fan.
   We will not use type classes or canonical structures because they
   count as "advanced" technology. But we will use notations.
 *)

(* We think of subsets as propositional functions.
   Thus, if [A] is a type [x : A] and [U] is a subset of [A],
   [U x] means "[x] is an element of [U]".
*)
Definition P (A : Type) := A -> Prop.