Cicada

Aims

• Libraries and tools for topological and geometric modeling

Community

• We enforce C4 as collaboration protocol -- The C4 RFC
• Style Guide -- observe the style of existing code and respect it
• Code of Conduct
• Source code -- github, gitlab
• cicada-rs -- an old version of the same project written in rust
• IRC -- #cicada-language
• CI -- gitlab-ci

Contributing

• Prepare: npm install
• Compile: npx tsc
• Compile and watch: npx tsc --watch
• Run all tests: npx ava
• Run specific test file: npx ava -sv <path to the test file>

Docs

• A Recursive Combinatorial Description of cell-complex
  • A paper about the definition of cell-complex in this project

Modules

• npm install cicada-lang

• API Docs

• Try examples

• Contents:

  • int
  • num
  • euclid
  • combinatorial-game
  • cell-complex
  • homology
  • cicadascript

int int

examples/int-module.js:

let assert = require ("assert") .strict

let ut = require ("cicada-lang/lib/util")
let int = require ("cicada-lang/lib/int")

{
  /**
   * generic `row_canonical_form`
   *   i.e. `hermite_normal_form` for integers
   */

  let A = int.matrix ([
    [2, 3, 6, 2],
    [5, 6, 1, 6],
    [8, 3, 1, 1],
  ])

  let B = int.matrix ([
    [1, 0, -11, 2],
    [0, 3, 28, -2],
    [0, 0, 61, -13],
  ])

  assert (
    A.row_canonical_form () .eq (B)
  )
}

{
  /**
   * generic `diag_canonical_form`
   *   i.e. `smith_normal_form` for integers
   */

  let A = int.matrix ([
    [2, 4, 4],
    [-6, 6, 12],
    [10, -4, -16],
  ])

  let S = int.matrix ([
    [2, 0, 0],
    [0, 6, 0],
    [0, 0, -12],
  ])

  assert (
    A.diag_canonical_form () .eq (S)
  )
}

{
  /**
   * solve linear diophantine equations
   */

  let A = int.matrix ([
    [1, 2, 3, 4, 5, 6, 7],
    [1, 0, 1, 0, 1, 0, 1],
    [2, 4, 5, 6, 1, 1, 1],
    [1, 4, 2, 5, 2, 0, 0],
    [0, 0, 1, 1, 2, 2, 3],
  ])

  let b = int.vector ([
    28,
    4,
    20,
    14,
    9,
  ])

  let solution = A.solve (b)

  if (solution !== null) {
    solution.print ()

    assert (
      A.act (solution) .eq (b)
    )
  }
}

num num

• with config-able epsilon for numerical stability

examples/num-linear-algebra.js:

let assert = require ("assert") .strict

let ut = require ("cicada-lang/lib/util")
let num = require ("cicada-lang/lib/num")

{
  /**
   * `reduced_row_echelon_form` reduces pivots to one
   *   while respecting `epsilon` for numerical stability
   */

  let A = num.matrix ([
    [1, 3, 1, 9],
    [1, 1, -1, 1],
    [3, 11, 5, 35],
  ])

  let B = num.matrix ([
    [1, 0, -2, -3],
    [0, 1, 1, 4],
    [0, 0, 0, 0],
  ])

  A.reduced_row_echelon_form () .print ()

  assert (
    A.reduced_row_echelon_form () .eq (B)
  )
}

eu euclid

• module theory over euclidean ring
  • for generic matrix algorithms

cg combinatorial-game

• a game engine for n-player perfect information games
• example games:
  • tic-tac-toe
  • hackenbush -- demo

cx cell-complex

• cell-complex based low dimensional algebraic topology library
• docs/a-recursive-combinatorial-description-of-cell-complex.md

gh graph

• [TODO]
• graph theory -- one dimensional cell-complex

hl homology

• cellular homology of cell-complex

examples/four-ways-to-glue-a-square.js:

• The following pictures are made by Guy Inchbald, a.k.a. Steelpillow

let cx = require ("cicada-lang/lib/cell-complex")
let hl = require ("cicada-lang/lib/homology")
let ut = require ("cicada-lang/lib/util")

class sphere_t extends cx.cell_complex_t {
  constructor () {
    super ({ dim: 2 })
    this.attach_vertexes (["south", "middle", "north"])
    this.attach_edge ("south_long", ["south", "middle"])
    this.attach_edge ("north_long", ["middle", "north"])
    this.attach_face ("surf", [
      "south_long",
      "north_long",
      ["north_long", "rev"],
      ["south_long", "rev"],
    ])
  }
}

class torus_t extends cx.cell_complex_t {
  constructor () {
    super ({ dim: 2 })
    this.attach_vertex ("origin")
    this.attach_edge ("toro", ["origin", "origin"])
    this.attach_edge ("polo", ["origin", "origin"])
    this.attach_face ("surf", [
      "toro",
      "polo",
      ["toro", "rev"],
      ["polo", "rev"],
    ])
  }
}

class klein_bottle_t extends cx.cell_complex_t {
  constructor () {
    super ({ dim: 2 })
    this.attach_vertex ("origin")
    this.attach_edge ("toro", ["origin", "origin"])
    this.attach_edge ("cross", ["origin", "origin"])
    this.attach_face ("surf", [
      "toro",
      "cross",
      ["toro", "rev"],
      "cross",
    ])
  }
}

class projective_plane_t extends cx.cell_complex_t {
  constructor () {
    super ({ dim: 2 })
    this.attach_vertexes (["start", "end"])
    this.attach_edge ("left_rim", ["start", "end"])
    this.attach_edge ("right_rim", ["end", "start"])
    this.attach_face ("surf", [
      "left_rim", "right_rim",
      "left_rim", "right_rim",
    ])
  }
}

• calculate homology groups:

let report = {
  "sphere": hl.report (new sphere_t ()),
  "torus": hl.report (new torus_t ()),
  "klein_bottle": hl.report (new klein_bottle_t ()),
  "projective_plane": hl.report (new projective_plane_t ()),
}

ut.log (report)

let expected_report = {
  sphere:
   { '0': { betti_number: 1, torsion_coefficients: [] },
     '1': { betti_number: 0, torsion_coefficients: [] },
     '2': { betti_number: 1, torsion_coefficients: [] },
     euler_characteristic: 2 },
  torus:
   { '0': { betti_number: 1, torsion_coefficients: [] },
     '1': { betti_number: 2, torsion_coefficients: [] },
     '2': { betti_number: 1, torsion_coefficients: [] },
     euler_characteristic: 0 },
  klein_bottle:
   { '0': { betti_number: 1, torsion_coefficients: [] },
     '1': { betti_number: 1, torsion_coefficients: [ 2 ] },
     '2': { betti_number: 0, torsion_coefficients: [] },
     euler_characteristic: 0 },
  projective_plane:
   { '0': { betti_number: 1, torsion_coefficients: [] },
     '1': { betti_number: 0, torsion_coefficients: [ 2 ] },
     '2': { betti_number: 0, torsion_coefficients: [] },
     euler_characteristic: 1 }
}

cs cicadascript

A dependently-typed programming language

• with javascript-like syntax
• based on game semantics
• for interactive theorem proving
• and practical verification tasks

examples (preview)

License

• GPLv3