expressions: Expressions and Formulae a la carte

[ bsd3, data, library, logic, math ] [ Propose Tags ]

This package is aimed at providing means of fixing a first-order language and declaring sorted expressions and formulae, the types ensure the declared expressions fall within the language.

This package pre-defines the common logical symbols for conjunction, disjunction, negation, and universal and existential quantification as well as some specific non-logical symbols such as equality, addition of linear integer arithmetic, and other. Common languages such as Lia and ALia (standard linear integer arithmetic and linear integer arithmetic with arrays) come included.

An example of a formula declaration:

-- Let's state that zero is successor to no integer (while this would be
-- true for non-negative integers, stated this way it is clearly false, but
-- it still is a well-formed first-order statement)

forall [var "x" :: Var 'IntegralSort] (cnst 0 ./=. var "x" .+. cnst 1) :: Lia 'BooleanSort

Let's see what declarations the library rejects:

(var "x" :: Lia 'BooleanSort) .=. (var "y" :: Lia 'IntegralSort)
(var "x" :: Lia 'BooleanSort) .=. (var "y" :: ALia 'BooleanSort)
forall [var "x" :: Var 'IntegralSort] true :: QFLia 'BooleanSort

Modules

[Last Documentation]

  • Data
    • Data.Expression
      • Data.Expression.Arithmetic
      • Data.Expression.Array
      • Data.Expression.Equality
      • Data.Expression.IfThenElse
      • Data.Expression.Parser
      • Data.Expression.Sort
      • Utils
        • Indexed
          • Data.Expression.Utils.Indexed.Eq
          • Data.Expression.Utils.Indexed.Foldable
          • Data.Expression.Utils.Indexed.Functor
          • Data.Expression.Utils.Indexed.Show
          • Data.Expression.Utils.Indexed.Sum
          • Data.Expression.Utils.Indexed.Traversable

Downloads

Maintainer's Corner

Package maintainers

For package maintainers and hackage trustees

Candidates

Versions [RSS] 0.1.1, 0.1.2, 0.1.3, 0.1.4, 0.1.5, 0.1.6, 0.1.7, 0.1.8, 0.1.9, 0.2, 0.3, 0.3.1, 0.4, 0.4.1, 0.4.2, 0.5
Change log ChangeLog.md
Dependencies attoparsec (>=0.13 && <0.14), base (>=4.11 && <4.13), containers (>=0.5.7 && <0.7), free (>=4.2 && <5.2), lattices (>=1.6 && <1.8), singletons (>=2.2 && <2.6), text (>=1.2 && <1.3), transformers (>=0.5.2 && <0.6) [details]
License BSD-3-Clause
Copyright Copyright (C) 2017 Jakub Daniel
Author Jakub Daniel
Maintainer jakub.daniel@protonmail.com
Category Data, Logic, Math
Source repo head: git clone https://github.com/jakubdaniel/expressions.git
Uploaded by jakubdaniel at 2018-10-03T07:39:48Z
Distributions
Reverse Dependencies 1 direct, 1 indirect [details]
Downloads 8376 total (36 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 2018-10-03 [all 3 reports]