Commit 8b2f6cf2 authored by Florian Rabe's avatar Florian Rabe

formalizations with Primoz

parent a038487f
namespace http://data.mathhub.info/schemas❚
theory ATDschema : ?MDDL =
meta ?MDDL?schemaGroup "GraphSym" ❙
/T We write G for the automorphism group of the digraph.❙
atd: Digraph ❘
meta ?Codecs?codec DigraphAsDigraph6 ❘
tag ?MDDL?opaque ❘
/T identifier❙
indexATD: string ❘
meta ?Codecs?codec StringIdent ❘
/T the number of vertices of the digraph❙
order: ℤ ❘
meta ?Codecs?codec IntIdent ❘
/T SelfOpp: true if the digraph is isomorphic to its opposite digraph❙
selfOpp: bool❘
meta ?Codecs?codec BoolAsYesNo❘
/T the name of the opposite digraph (the same as "Name" if the digraph is self-opposite❙
oppATD: string ❘
meta ?Codecs?codec StringIdent ❘
/T true if the undirected graph is arc-transitive❙
isUndAT: bool❘
meta ?Codecs?codec BoolAsYesNo❘
/T the name of the underlying graph, as given in the files "Census-HAT-1k-data.csv" and "Census-GHAT-1k-data.csv" --
if the underlying graph is generalized wreath, then this is indicated by, say, "GWD(m,k)" where m and k are the defining parameters.
undGph: graph ❘
meta ?Codecs?codec Expression ❘
/T the largest integer s, such that the digraph is s-arc-transitive❙
s: ℤ ❘
meta ?Codecs?codec IntIdent ❘
/T true if the vertex-stabiliser G_v in the full automorphism group G of the digraph is abelian ("Ab/"n-Ab" in readme file)❙
GvAb: bool ❘
meta ?Codecs?codec BoolIdent ❘
/T the index of G in the smallest arc-transitive group T of the underlying graph that contains G -- if there's no such group T, then "0"❙
TvGv: ℤ ❘
meta ?Codecs?codec IntIdent ❘
/T the index of G in the automorphism group of the underlying graph❙
AvGv: ℤ ❘
meta ?Codecs?codec IntAsDigitListAndFactorList ❘
/T true if G is solvable ("solve"/"n-solv" in readme file)❙
solv: bool ❘
meta ?Codecs?codec BoolIdent ❘
/T the next four fields are about alternating cycles❙
/T half of the length of the alternating cycle❙
rad: ℤ ❘
meta ?Codecs?codec IntIdent ❘
/T AtNo: this one is the size of the intersection of two intersecting alternating cycles❙
AtNo❙
/T "loose" if AtNo=1, "antipodal" if AtNo=2, and "tight" if AtNo=rad, otherwise "---"❙
AtTy: FiniteType "loose" "antipodal" "tight" "---" ❘
meta ?Codecs?codec FiniteTypeCodec StringIdent ❘
/T |AltCyc|: the number of alternating cycles❙
AltCyc❙
/T the next three fields are about the alter-relations❙
/T the alter-exponent❙
AltExp❙
/T the alter-perimeter❙
Altper❙
/T the alter-sequence ❙
AltSeq: list ℤ ❘
meta ?Codecs?codec ListAsArray IntIdent ❘
/T true if the digraph is generalized wreath❙
IsGWD❘
meta ?Codecs?codec BoolAsYesNo
\ No newline at end of file
......@@ -46,15 +46,30 @@ theory MathData : ?Framework =
matrix : type ⟶ int ⟶ int ⟶ type ❘= [a,m,n] vector (vector a m) n❙
option : type ⟶ type❙
some : {a} a ⟶ option a❙
none : {a} option a❙
some : {a} a ⟶ option a❙
none : {a} option a❙
getOrElse : {a} option a ⟶ a ⟶ a❙
ifknown : type ⟶ type❙
known : {a} a ⟶ ifknown a❙
unknown : {a} ifknown a❙
getIfKnown : {a} ifknown a ⟶ a ⟶ a❙
finset : type ⟶ type❙
product : type ⟶ type ⟶ type❘# 1 * 2❙
pair : {a,b} a ⟶ b ⟶ product a b❘# 3 , 4❙
left : {a,b} product a b ⟶ a ❘# 3 _1❙
right : {a,b} product a b ⟶ b❘# 3 _2❙
pair : {a,b} a ⟶ b ⟶ product a b❘# 3 , 4❙
left : {a,b} a * b ⟶ a ❘# 3 _1❙
right : {a,b} a * b ⟶ b❘# 3 _2❙
dunion : type ⟶ type ⟶ type ❘# 1 ∪ 2❙
inLeft : {a,b} a ⟶ a ∪ b❙
inRight : {a,b} b ⟶ a ∪ b❙
dunion_cases: {a,b,c: type} a∪b ⟶ (a ⟶ c) ⟶ (b ⟶ c) ⟶ c❙
finiteType: type ⟶ type❙
/T finiteType a must be subtype of a❙
Ring = {'
univ: type,
plus: univ ⟶ univ ⟶ univ,
......@@ -121,14 +136,19 @@ theory Codecs : ur:?PLF =
StringIdent : codec string db_string❙
UUIDIdent : codec uuid db_uuid❙
IntAsString : codec int db_string❙
/T encodes booleans as "Yes" or "No"❙
BoolAsYesNo : codec bool db_string❙
ListAsArray : {A,a} codec A a ⟶ codec (list A) (db_array a)❘# ListAsArray 3❙
VectorAsArray : {A,a,n} codec A a ⟶ codec (vector A n) (db_array a)❘# VectorAsArray 3 4❙
OptionAsNullable : {A,a} codec A a ⟶ codec (option A) a❘# OptionAsNullable 3❙
ProductAsArray: {A,B,e} codec A e ⟶ codec B e ⟶ codec (A * B) e❙
MatrixAsArray : {A,a,m,n} codec A a ⟶ codec (matrix A m n) (db_array (db_array a))❘
= [A,a,m,n,C] VectorAsArray n (VectorAsArray m C)❘# MatrixAsArray 5❙
FiniteTypeAsItself : {A,a} codec A a ⟶ codec (finiteType A) a❙
FinSetAsArray : {A,a} codec A a ⟶ codec (finset A) (db_array a)❙
PolynomialAsSparseArray : {r, e} codec (r.univ) e ⟶ codec (Poly r) (db_array (db_array e))❘# %%prefix 2 1❙
PolynomialAsDenseArray : {r, e} codec (r.univ) e ⟶ codec (Poly r) (db_array e)❘# %%prefix 2 1❙
......
......@@ -3,6 +3,9 @@ namespace http://data.mathhub.info/schemas❚
/T Nodes on formalizing graphs from scratch made during Primož Potočnik's visit in May 2019.
This was a quick exercise to get a feel for the system and still has lots of errors.❚
/T a quick stub of a background math theory,
this should be part of a larger theory elsewhere but is kept here for now to be self-contained❚
theory BackgroundMath : ur:?LF =
set: type❙
prop: type❙
......@@ -18,8 +21,74 @@ theory BackgroundMath : ur:?LF =
image : {A} (elem A ⟶ set) ⟶ set❙
those : {A} (elem A ⟶ prop) ⟶ elem ℘ A❙
ℕ : type❙
/T {0,...n-1}, subtype of ℕ❙
upto : ℕ ⟶ type❙
theory Graphs : ?BackgroundMath =
arc : type❘= ℕ * ℕ❙
edge : type❙
opp : arc ⟶ arc❘ = [a] (right a, left a)❙
opp_opp: {a} ⊦ opp opp a = a❘= [a] _❙
toEdge : arc ⟶ edge❘= [a] uopair a.1 a.2❙
theory StandardDiGraph : ?BackgroundMath =
order: ℕ❘
nodes: type❘= upto order❙
arcs: finset (nodes*nodes)❙
edges: finset (nodes*nodes)❘= arcs map toEdge❙
theory StandardGraph : ?BackgroundMath =
include ?StandardDiGraph❙
symmetric: ⊦ forall [a] a ∈ arcs ⇒ opp a ∈ arcs❙
digraph: type❘= Mod(StandardGraph)❙
graph: type❘= Mod(StandardGraph)❙
opposite : digraph ⟶ digraph❘# Opp 1❘
= [g] ['
order = g.order,
arcs = g.arcs map opp
']❙
theory DiGraphHom(g: digraph, h: digraph) : ?BackgroundMath =
nodes : g.nodes ⟶ h.nodes❙
arcMap : g.arcs ⟶ h.arcs ❘= [a] (nodes a.1, nodes a.2)❙
arcs : ⊦ forall [a] a ∈ g.arcs ⇒ arcMap a ∈ h.arcs❙
theory DiGraphIso(g: digraph, h: digraph) : ?BackgroundMath =
include ?DiGraphHom❙
iso : isbijection nodes❙
auto : digraph ⟶ type❘= [g] Mod(DiGraphIso(g,g))❙
isomorphic : digraph ⟶ digraph ⟶ prop❘# 1 ≅ 2❘
= [g,h] nonempty Mod(DiGraphIso(g,h))❙
selfOpp : digraph ⟶ prop ❘= [g] Opp Opp g ≅ g❙
underlying : digraph ⟶ graph❘
= [d] ['
order = d.order,
arcs = d.arcs ∪ (d.arcs map opp),
symmetric = forallI [a] impI [p]
p unionE ([q] unionI_right mapI q)
([q] unionI_left opp_opp q)
']❙
arcTransitive : digraph ⟶ prop❘
= [g] ∀ [a] a ∈ g.arcs ⇒ ∀ [b] b ∈ g.arcs ⇒ ∃ [i: auto g] i.arcMap a = b❙
/T Sketches of some alternative definitions we discussed.❚
theory DiGraph1 : ?BackgroundMath =
node: set❙
edge: set❙
......@@ -76,18 +145,3 @@ theory DiGraph4 : ?BackgroundMath =
node: set❙
edges: elem list (node * node)❙
theory CodecExamples =
PairAsArray : {A,B,c} codec A c ⟶ codec B c ⟶ codec (A*B) (array c)❙
FinSetAsArray : {A,a} codec A a ⟶ codec (FinSet A) (array a)❙
theory DiGraphIsoType : ?BackgroundMath =
order: ℕ❘
meta codec NatAsInt❙
nodes: type❘= upto order❙
edges: FinSet (nodes*nodes)❘
meta codec FinSetAsArray (PairAsArray NatAsInt NatAsInt)❙
\ No newline at end of file
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment