conal/denotational-hardware

Denotational hardware design in Agda

denotational-hardware's Issues

Prove laws for functions

See stub module Functions.Laws.

CoCartesian and BiCartesian Categories

When working on #21 I figured that having CoCartesian Categories, hence coproducts and even BiCartesian Categories formalized it would be more elegant to express some of the fields and laws of Logic. However adding CoCartesian to Categorical.{Raw,Laws} isn't trivial due to name clashing. A couple of possible solutions are:

• Put Cartesian and CartesianClosed in a local module called Cartesian and create a second local module called CoCartesian as well.
• Obtain the CoCartesian formalization via dualization
• more?

Set up continuous integration

Perhaps there are recommendations and examples for Agda projects on GitHub.

Laws from homomorphisms

Given a homomorphism with lawful target, if equivalence of source morphisms is defined via the same homomorphism (f ≈ g = Fₘ f ≈ Fₘ g), then the source must also be lawful. Categorical.MakeLawful implements/proves this fact for Category. Next, prove it for Cartesian, CartesianClosed, etc.

Homomorphism proofs for Linearize

See stub module in Routing.Homomorphism.

Mixed-category developments

Comma categories allow mixing different categories into a single package of specification, implementation, and correctness proof. For instance,

• Functions can implement relations.
• Matrices can implement functions.
• Mealy machines can implement functions.

Identify simple concrete examples of such multi-category developments, implement the categories involved, and build some arrow morphisms.

CartesianH for Routing

Building on the work of PR #10 (providing a CategoryH instance for the routing category), continue with CartesianH.

Refinement

Can commutative diagrams (and thus comma categories) somehow capture refinement, in which the implementation is more specific than (and thus entails) the specification? If not, is there another category-theoretic notion that does subsume refinement?

Categorical.Laws

Fill in Categorical.Laws.

CategoryH proofs for Routing

See stub module in Routing.Homomorphism.

Hyperlinked source code

Set up our project to generate highlighted and hyperlinked source code HTML and deploy on github.io in the manner of agda-stdlib.

Compact proofs in `Categorical.Laws`

... using the helpers in Categorical.Reasoning. Doing so will speed up loading and hopefully be easier to read.

Vector category

Define a parametrized cartesian category of vectors and vector functions, in which the objects are natural numbers denoting vectors (from Data.Vec) of the given length, with the element type given by a module parameter. Define a denotation as a cartesian functor to functions.

Later, we can build up from this category to hardware designs, specializing the element type to Bool.

Homomorphism proofs for Primitive

See stub module in Primitive.Homomorphism.