Evan Patterson epatters
epatters
/ category_phl.egg
Created
May 6, 2025 00:16
Categories in egglog using partial Horn logic (PHL)
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| (datatype Ob (ObGen String)) | |
| (datatype Mor (MorGen String)) | |
| (constructor dom (Mor) Ob) | |
| (constructor cod (Mor) Ob) | |
| (constructor id (Ob) Mor) | |
| (constructor compose (Mor Mor) Mor) | |
| (ruleset CatAxioms) | |
| ; Predicate: Is a morphism term well-typed? |
epatters
/ direct_product_monoid.egg
Created
April 17, 2025 23:18
Direct product of monoids of signs and natural numbers, using egglog
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| ; Theory of monoids | |
| (datatype Mon | |
| (Gen String) | |
| (times Mon Mon) | |
| (unit)) | |
| ; The usual monoid axioms, but note that the associativity rewrite is bidirectional, | |
| ; whereas the unit rewrites are unidirectional. This ensures that the rewrites never increase | |
| ; the size of the expressions, so we can safely saturate the e-graph. | |
| (ruleset MonAxioms) |
epatters
/ functor.egg
Created
April 16, 2025 06:33
Model refinement by finitely presented functor, using egglog
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| ; Theory of a category: first copy, for the domain category | |
| ; (Associativity and unitality axioms not recorded.) | |
| (datatype Ob1 (ob1 String)) | |
| (datatype Mor1 (mor1 String)) | |
| (constructor dom1 (Mor1) Ob1) | |
| (constructor cod1 (Mor1) Ob1) | |
| (constructor id1 (Ob1) Mor1) | |
| (rewrite (dom1 (id1 x)) x) | |
| (rewrite (cod1 (id1 x)) x) |
epatters
/ gat_statechart_hazards.jl
Created
June 5, 2024 16:46
Using GATLab to create symbolic expressions for the hazard rates attached to a statechart
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| using Catlab | |
| import Base: +, -, ~, zero | |
| import Catlab: ⋅ | |
| """ Theory of the commutative algebra of quantities. | |
| """ | |
| @theory ThQuantityAlgebra begin | |
| Quantity::TYPE | |
| # Multiplicative commutative monoid. |
epatters
/ sir_network_migration.jl
Created
May 29, 2024 14:43
Migrating rules for SIR models on networks
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| using Catlab, DataMigrations | |
| # SIR | |
| ##### | |
| @present SchSIR(FreeSchema) begin | |
| Person::Ob | |
| (S, I, R)::Ob | |
| S_is_person::Hom(S, Person) | |
| I_is_person::Hom(I, Person) |
epatters
/ port_graph_migration.ipynb
Created
February 10, 2022 20:43
Migrating graphs to port graphs
Loading
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.
epatters
/ pullback_stratify.ipynb
Created
October 21, 2021 18:29
Stratification using pullbacks: toy example
Loading
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.