cmu: Unification in a Commutative Monoid

[ algebra, library, program ] [ Propose Tags ]

The unification problem is given the problem statement t =? t', find a most general substitution s such that s(t) = s(t') modulo the axioms of a commutative monoid. Substitition s is more general than s' if there is a substitition s" such that s' = s" o s.

[Skip to Readme]

Versions [faq]	1.0, 1.1, 1.2, 1.3, 1.4, 1.5, 1.6, 1.7, 1.8, 1.9, 1.10, 1.11, 1.12
Change log	ChangeLog
Dependencies	array, base (>=4.13 && <5), containers (>=0.3) [details]
License	LicenseRef-GPL
Author
Maintainer	ramsdell@mitre.org
Category	Algebra
Source repo	head: git clone git://github.com/ramsdell/cmu.git
Uploaded	by JohnRamsdell at Thu Oct 17 16:46:14 UTC 2019
Distributions	NixOS:1.12
Executables	cmu
Downloads	7522 total (318 in the last 30 days)
Rating	(no votes yet) [estimated by Bayesian average]
Your Rating	λ λ λ
Status	Docs not available [build log] All reported builds failed as of 2019-10-17 [all 3 reports]

Modules

Algebra
- CommutativeMonoid
  - Algebra.CommutativeMonoid.LinDiophEq
  - Algebra.CommutativeMonoid.Unification

Downloads

cmu-1.12.tar.gz [browse] (Cabal source package)
Package description (as included in the package)

Maintainer's Corner

For package maintainers and hackage trustees

edit package information

Readme for cmu-1.12

[back to package description]

This package contains a library for unification in
commutative monoid and a program that exercises the library.

$ cmu
Commutative monoid unification -- :? for help
cmu> 2x+y=3z
Problem:   2x + y = 3z
Unifier:   [x : g0 + 3g2,y : g0 + 3g1,z : g0 + g1 + 2g2]

cmu> 2x=x+y
Problem:   2x = x + y
Unifier:   [x : g0,y : g0]

cmu> 64x=41y+a
Problem:   64x = a + 41y
Unifier:   [a : 5g0 + 2g1 + 23g2 + g3 + 64g4,x : 2g0 + 9g1 + g2 + 25g3 + g4 + 41g5,y : 3g0 + 14g1 + g2 + 39g3 + 64g5]

cmu> :quit