Rules and Inference

Rules express how new facts follow from existing ones. Together with relations, they form the core of a Fixen program: relations declare what facts look like, and rules declare how they propagate.

Rule Syntax

A rule has the form:

rule name arg1 ... argm: p1, ..., pn, if c1, ..., if ck |- conclusion

• The rule keyword introduces the declaration.
• An optional name after rule identifies the rule (used by priorities and phases, see Priorities and Phases).
• An optional parameter list arg1 to argm after the rule name specifies the parameters to the rule to be instantiated by premises of the rule. If no parameter list is specified, it will be inferred by the premises of the rule. Explicitly specifying rule parameters can improve readability and also allows the compiler check for typos in the rule premises, e.g., using the wrong variable name.
• Zero or more premises p1 to pn are relations applied to variables, separated by commas. They specify what relations must be satisfied by the program for the rule to fire.
• Zero or more if guards specify boolean conditions c1 to ck. These restrict firing to cases where Haskell expressions evaluate to True.
• The turnstile |- separates premises and boolean conditions from the conclusion — the fact to derive.

Example: Reachability Rules

Continuing from the reachability example in Relations and Facts, we need two rules:

rule edgeToPath: Edge a b |- Path a b
rule pathStep: Edge a b, Path b c |- Path a c

The first rule, edgeToPath, states that every edge is also a path. The second rule, pathStep, performs transitive closure: if there is an edge from a to b and a path from b to c, then there is a path from a to c.

Variables and Matching

Variables in Fixen rules follow Haskell naming conventions: identifiers starting with a lowercase letter (e.g., u, v, vertex). A variable appearing in multiple premises must match the same value in all of them. This is how rules express dependencies between facts.

In pathStep, the variable b appears in both the Edge premise and the Path premise. The rule fires only when there exists a fact Edge a b and a fact Path b c where the b values are identical. The shared variable acts as a join key, connecting the two relations.

How Rules Fire

The Fixen solver applies rules in a forward-chaining loop:

1. Starting from the initial facts provided to solve, the solver checks which rules can fire.
2. When a rule fires, its conclusion is added to the fact database if it is not already present or subsumed by existing facts.
3. New facts may enable additional rules to fire.
4. This continues until no new facts can be derived — a fixed point is reached.

For the reachability program, the solver proceeds roughly as follows:

1. edgeToPath fires for every Edge fact, populating Path with direct connections.
2. pathStep fires for every combination of Edge a b and Path b c facts, deriving Path a c.
3. As pathStep derives new Path a c facts, they enable further pathStep firings, extending paths transitively.
4. The loop terminates when no new paths can be derived.

Explicit Parameters

Rules can declare their variables explicitly after the rule name:

rule pathStep: Edge a b, Path b c |- Path a c

This is equivalent to the implicit version above. Explicit parameters can improve readability for rules with many variables, though most Fixen programs use the implicit form.

Haskell Expressions in Rules

Boolean conditions and conclusions can include Haskell expressions, which the solver evaluates when the rule fires:

rule combine: Path a b, Path b c, if (a ++ b) == "abc" |- Path a (b ++ ("-" ++ c))

The expressions (a ++ b) == "abc" and b ++ ("-" ++ c) is evaluated as Haskell code using the instantiated variable values. See Haskell Interop for details on embedding Haskell in your programs.

Note

Haskell expressions in rules are currently limited to variables, function application, integer and string literals, tuples, lists, and the unit value. Function application includes infix notation: x + y, x `op` y, and any valid Haskell operator are supported.

However, Fixen has no knowledge of Haskell’s operator precedence or fixity declarations. All expressions must be easily parseable without knowing fixity. This means operands must be parenthesized when chaining operations: write (1 + 2) + 3 instead of 1 + 2 + 3. Simple expressions like x + y or [1] ++ [3] are unambiguous and always parse correctly.

Turnstiles

The turnstile |- is a valid Haskell operator and thus can be part of a Haskell expression. Any expression that uses |- must be parenthesized.

Complete Example: Graph Reachability

We have everything we need to write a complete work-queue algorithm with Fixen.

Download: reachability.tar.gz

SHA-256: 397310a2db09c8c471e8a5e6fc4cf5431e5288111642f420daf0ebaf13690fc8

Project Setup

First, set up a cabal project with the following structure:

• Directoryreachability

  • reachability.cabal
  • Directoryapp

    • Main.hs
  • Directoryfix

    • Reachability.fix

The project configuration can be as follows. Note the other-modules and build-depends fields:

reachability.cabal

cabal-version:      3.0
name:               reachability
version:            0.1.0.0
build-type:         Simple
common warnings
    ghc-options: -Wall
executable reachability
    import:           warnings
    main-is:          Main.hs
    other-modules:    Reachability
    build-depends:    base
                    , pqueue
                    , unordered-containers
    hs-source-dirs:   app
    default-language: GHC2021

Fixen Program

Our Fixen program will consist of the relations and rules seen in the previous examples; these compute reachable vertices in a graph:

fix/Reachability.fix

module Reachability where

```hs
type Vertex = String
```

rel Edge: Vertex, Vertex
rel Path: Vertex, Vertex

rule edgeToPath: Edge a b |- Path a b
rule pathStep: Edge a b, Path b c |- Path a c

query allPaths: Path - -

Note the last line of fix/Reachability.fix: this is a query which allows us to obtain all Path facts from the solved fact database. We describe queries in more detail in Queries.

Then, from the root directory of the project, compile fix/Reachability.fix as a Haskell module app/Reachability.hs:

Terminal

~/reachability $ fixen --output app/Reachability.hs fix/Reachability.fix

Completing the Program

To complete the program, our driver module app/Main.hs will:

1. Instantiate edges of our graph as Edge facts
2. Solve for all facts starting from our edge facts using the Fixen-generated solve function
3. Print all Path facts using the allPaths query:

app/Main.hs

module Main where

import Reachability

main :: IO ()
main = do
  let edges = [ Edge "Paris" "Tokyo"
              , Edge "Tokyo" "New York" ]
  let solved_database = solve edges
  print (allPaths solved_database)

Running the Program

Run the program using cabal run. We should expect to see paths from:

• Paris to Tokyo (given by the first edge)
• Tokyo to New York (given by the second edge)
• Paris to New York (by taking the preceding edges)

Terminal

~/reachability $ cabal run
[Path "Tokyo" "New York",Path "Paris" "Tokyo",Path "Paris" "New York"]

Summary

• Rules derive new facts from existing ones using premises and a conclusion.
• Variables (lowercase identifiers) connect premises through matching.
• Rules fire forward-chaining until a fixed point is reached.
• Haskell expressions in conclusions enable computation within rules.
• The name of a rule is optional but becomes important when using Priorities.