Skip to content

Commit

Permalink
Update obvinf.hpp for v1/3
Browse files Browse the repository at this point in the history
  • Loading branch information
james-d-mitchell committed Sep 20, 2024
1 parent cfdda4c commit ded0e6e
Show file tree
Hide file tree
Showing 7 changed files with 287 additions and 4 deletions.
1 change: 1 addition & 0 deletions docs/source/data-structures/misc/index.rst
Original file line number Diff line number Diff line change
Expand Up @@ -14,6 +14,7 @@ In this section we describe some miscellaneous functionality in
:maxdepth: 1

constants
obvinf
runner
reporter

Expand Down
58 changes: 58 additions & 0 deletions docs/source/data-structures/misc/obvinf.rst
Original file line number Diff line number Diff line change
@@ -0,0 +1,58 @@
.. Copyright (c) 2024 J. D. Mitchell
Distributed under the terms of the GPL license version 3.
The full license is in the file LICENSE, distributed with this software.
.. currentmodule:: _libsemigroups_pybind11

Obviously infinite
==================

This page collects the documentation for the functionality in
``libsemigroups_pybind11`` for checking if a finitely presented semigroup or
monoid is obviously infinite.

The functions below implement a number of checks for whether or not a finitely
presented semigroup or monoid is infinite. These checks are all decidable, and
always return an answer within an amount of time that is linear in the size of
the input.

These checks are:

1. For every generator there is at least one side of one relation that
consists solely of that generator. If this condition is not met, then
there is a generator of infinite order.

2. The number of occurrences of every generator is not preserved by the
relations. Otherwise, it is not possible to use the relations to
reduce the number of occurrences of a generator in a word, and so
there are infinitely many distinct words.

3. The number of generators on the left hand side of a relation is not
the same as the number of generators on the right hand side for at
least one generator. Otherwise the relations preserve the length of
any word and so there are infinitely many distinct words.

4. There are at least as many relations as there are generators.
Otherwise we can find a surjective homomorphism onto an infinite
subsemigroup of the rationals under addition.

5. The checks 2., 3. and 4. are a special case of a more general matrix
based condition. We construct a matrix whose columns correspond to
generators and rows correspond to relations. The ``(i, j)``-th entry is
the number of occurrences of the ``j``-th generator in the left hand side
of the ``i``-th relation minus the number of occurrences of it on the
right hand side. If this matrix has a non-trivial kernel, then we can
construct a surjective homomorphism onto an infinite subsemigroup of
the rationals under addition. So we check that the matrix is full
rank.

6. The presentation is not that of a free product. To do this we consider
a graph whose vertices are generators and an edge connects two
generators if they occur on either side of the same relation. If this
graph is disconnected then the presentation is a free product and is
therefore infinite. Note that we currently do not consider the case
where the identity occurs in the presentation.

.. autofunction:: is_obviously_infinite
25 changes: 21 additions & 4 deletions src/knuth-bendix.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -555,10 +555,27 @@ is returned.
"is_obviously_infinite",
[](KnuthBendix<Rewriter>& kb) { return is_obviously_infinite(kb); },
R"pbdoc(
:sig=(kb: KnuthBendixRewriteTrie):
:only-document-once:
TODO
)pbdoc");
:sig=(kb: KnuthBendixRewriteTrie) -> bool:
Function for checking if the quotient of a finitely presented
semigroup or monoid defined by a :any:`KnuthBendix` object is obviously infinite
or not.
This function returns ``True`` if the quotient of the finitely presented
semigroup or monoid defined by the :any:`KnuthBendix` object *kb* is obviously
infinite; ``False`` is returned if it is not.
:param kb: the :any:`KnuthBendix` instance.
:type kb: KnuthBendix
:returns:
Whether or not the quotient defined by a :any:`KnuthBendix` instance is
obviously infinite.
.. note::
If this function returns ``False``, it is still possible that the quotient
defined by the :any:`KnuthBendix` object *kb* is infinite.
)pbdoc");
}
} // namespace

Expand Down
1 change: 1 addition & 0 deletions src/main.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -148,6 +148,7 @@ namespace libsemigroups {
init_gabow(m);
init_knuth_bendix(m);
init_order(m);
init_obvinf(m);
init_paths(m);
init_present(m);
init_inverse_present(m);
Expand Down
1 change: 1 addition & 0 deletions src/main.hpp
Original file line number Diff line number Diff line change
Expand Up @@ -49,6 +49,7 @@ namespace libsemigroups {
void init_freeband(py::module&);
void init_dot(py::module&);
void init_matrix(py::module&);
void init_obvinf(py::module&);

} // namespace libsemigroups

Expand Down
148 changes: 148 additions & 0 deletions src/obvinf.cpp
Original file line number Diff line number Diff line change
@@ -0,0 +1,148 @@
//
// libsemigroups_pybind11
// Copyright (C) 2024 James Mitchell
//
// This program is free software: you can redistribute it and/or modify
// it under the terms of the GNU General Public License as published by
// the Free Software Foundation, either version 3 of the License, or
// (at your option) any later version.
//
// This program is distributed in the hope that it will be useful,
// but WITHOUT ANY WARRANTY; without even the implied warranty of
// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
// GNU General Public License for more details.
//
// You should have received a copy of the GNU General Public License
// along with this program. If not, see <http://www.gnu.org/licenses/>.
//

// libsemigroups headers
#include <libsemigroups/cong.hpp>
#include <libsemigroups/kambites.hpp>
#include <libsemigroups/obvinf.hpp>
#include <libsemigroups/todd-coxeter.hpp>

// pybind11....
#include <pybind11/pybind11.h>

// libsemigroups_pybind11....
#include "main.hpp" // for init_obvinf

namespace py = pybind11;

namespace libsemigroups {

void init_obvinf(py::module& m) {
m.def(
"is_obviously_infinite",
[](Presentation<word_type> const& p) {
return is_obviously_infinite(p);
},
R"pbdoc(
:sig=(p: PresentationStrings) -> bool:
Function for checking if the finitely presented semigroup or monoid
defined by a :any:`Presentation` object is obviously infinite or not.
This function returns ``True`` if the finitely presented semigroup or
monoid defined by the :any:`Presentation` object *p* is obviously infinite.
:param p: the presentation.
:type p: Presentation
:returns:
Whether or not the presentation defines an obviously infinite semigroup or
monoid.
:rtype:
bool
:raises LibsemigroupsError: If the presentation *p* is not valid.
.. note::
If this function returns ``False``, it is still possible that semigroup or
monoid defined by *p* is infinite.
)pbdoc");

m.def(
"is_obviously_infinite",
[](ToddCoxeter const& tc) { return is_obviously_infinite(tc); },
py::arg("tc"),
R"pbdoc(
:sig=(p: ToddCoxeter) -> bool:
Function for checking if the quotient of a finitely presented semigroup or
monoid defined by a :any:`ToddCoxeter` object is obviously infinite or not.
This function returns ``True`` if the quotient of the finitely presented
semigroup or monoid defined by the :any:`ToddCoxeter` object *tc* is obviously
infinite; ``False`` is returned if it is not.
:param tc: the ToddCoxeter instance.
:type tc: ToddCoxeter
:returns:
Whether or not the quotient defined by a :any:`ToddCoxeter` instance is
obviously infinite.
.. note::
If this function returns ``False``, it is still possible that the quotient
defined by the ToddCoxeter object *tc* is infinite.
)pbdoc");

m.def(
"is_obviously_infinite",
[](Congruence& c) { return is_obviously_infinite(c); },
py::arg("c"),
R"pbdoc(
:sig=(c: Congruence) -> bool:
Function for checking if a congruence obviously has infinite many
classes.
This function returns ``True`` if the quotient of the finitely presented
semigroup or monoid defined by the :any:`Congruence` object *c* is obviously
infinite; ``False`` is returned if it is not.
:param c: the :any:`Congruence` instance.
:type c: Congruence
:returns:
Whether or not the congruence obviously has infinitely many
classes.
.. note::
If this function returns ``False``, it is still possible that the
congruence has infinitely many classes.
)pbdoc");

m.def(
"is_obviously_infinite",
[](Kambites<detail::MultiStringView>& k) {
return is_obviously_infinite(k);
},
py::arg("k"),
R"pbdoc(
:sig=(k: Kambites) -> bool:
Function for checking if the finitely presented semigroup or
monoid defined by a :any:`Kambites` object obviously has infinite many
classes.
This function returns ``True`` if the finitely presented semigroup or
monoid defined by a :any:`Kambites` object is obviously infinite; ``False`` is
returned if it is not.
:param k: the :any:`Kambites` instance.
:type k: Kambites
:returns:
Whether or not the finitely presented semigroup or monoid defined by a
:any:`Kambites` object is obviously infinite.
.. note::
If this function returns ``False``, it is still possible that finitely
presented semigroup or monoid defined by *k* is infinite.
)pbdoc");
} // init_obvinf

} // namespace libsemigroups
57 changes: 57 additions & 0 deletions tests/test_obvinf.py
Original file line number Diff line number Diff line change
@@ -0,0 +1,57 @@
# -*- coding: utf-8 -*-
# Copyright (c) 2024 J. D. Mitchell
#
# Distributed under the terms of the GPL license version 3.
#
# The full license is in the file LICENSE, distributed with this software.

"""
This module contains some tests for the functions is_obviously_infinite.
"""

# pylint: disable=missing-function-docstring, duplicate-code

from libsemigroups_pybind11 import (
Presentation,
presentation,
is_obviously_infinite,
congruence_kind,
KnuthBendix,
ReportGuard,
)


def test_is_obviously_infinite_presentation():
p = Presentation([0, 1])
presentation.add_rule(p, [0], [0, 1, 1])
presentation.add_rule(p, [1], [1, 0, 0])

assert not is_obviously_infinite(p)

p = Presentation([0, 1, 2, 3, 4])
presentation.add_rule(p, [0], [0] * 2)
presentation.add_rule(p, [1], [1] * 2)
presentation.add_rule(p, [0, 1, 4], [4] * 3)
presentation.add_rule(p, [3, 2], [2])
presentation.add_rule(p, [2, 2], [3, 3, 3])

assert is_obviously_infinite(p)


def test_is_obviously_infinite_knuth_bendix():
ReportGuard(False)

p = Presentation("abABe")
p.contains_empty_word(True)
presentation.add_identity_rules(p, "e")
presentation.add_inverse_rules(p, "ABabe", "e")
presentation.add_rule(p, "aaa", "")
presentation.add_rule(p, "bbb", "")
presentation.add_rule(p, "abababab", "")
presentation.add_rule(p, "aBaBaBaBaB", "")

kb = KnuthBendix(congruence_kind.twosided, p)

assert not is_obviously_infinite(kb)
assert kb.number_of_classes() == 1080
assert not is_obviously_infinite(kb)

0 comments on commit ded0e6e

Please sign in to comment.