# Temporal Reasoning

Facts don't always stay true forever. Employees change teams. Certifications
expire. Systems go up and down. Mangle's temporal reasoning extension lets you
track *when* things are true, not just *that* they're true.

## Temporal Facts

Add a time interval to any fact with `@[start, end]`:

```
# Alice was on engineering from Jan 2020 to June 2023
team_member(/alice, /engineering)@[2020-01-01, 2023-06-15].

# Bob joined engineering in 2019 and is still there
team_member(/bob, /engineering)@[2019-06-01, _].

# Something that happened at a specific moment
login(/alice)@[2024-03-15T10:30:00].

# Currently active (from 2024 until now)
active(/alice)@[2024-01-01, now].

# Something happening right now
logged_in(/bob)@[now].
```

Special bounds:
- `_` means unbounded (beginning of time or ongoing into the future)
- `now` means the current evaluation time

Facts without `@[...]` work exactly like before - they're eternal truths.

### Note on Date Semantics

When using a date without a time (e.g., `2024-01-01`), it is interpreted as **midnight (00:00:00) at the start of that day**.

Since Mangle uses inclusive intervals `[start, end]`:
- `@[2024-01-01, 2024-01-01]` is a single point in time (midnight).
- `@[2024-01-01, 2024-01-02]` covers exactly 24 hours + 1 nanosecond (from midnight Jan 1 to midnight Jan 2).
- To include the entirety of Jan 31st, use `2024-02-01` as the end bound (covering up to midnight of the next day).

## Temporal Operators

Four operators let you reason about time:

### Past Operators

**Diamond-minus `<-`** - "was true at some point in the past"

```
# Was active sometime in the last 30 days
recently_active(X) :- <-[0d, 30d] active(X).
```

**Box-minus `[-`** - "was true continuously in the past"

```
# Was continuously active for the last 30 days
reliably_active(X) :- [-[0d, 30d] active(X).
```

### Future Operators

**Diamond-plus `<+`** - "will be true at some point in the future"

```
# Will be on maintenance sometime in the next 7 days
maintenance_pending(X) :- <+[0d, 7d] maintenance(X).
```

**Box-plus `[+`** - "will be true continuously in the future"

```
# Contract will be valid for the entire next 30 days
covered(X) :- [+[0d, 30d] contract(X).
```

The interval `[0d, 30d]` means "from now to 30 days ago/ahead". You can use:
- `d` for days
- `h` for hours
- ISO timestamps like `2024-01-15T10:30:00`

## Evaluation Time and "now"

Rules that use temporal operators with relative durations (like `<-[7d]`) depend on a reference point called `now`. This `now` corresponds to the moment for which you are evaluating the policy or query.

Because these rules are relative to `now`, the resulting set of derived facts represents the state of the world **at that specific point in time**.

For example, if you run a query asking for "users active in the last 7 days", the result is a snapshot valid for the moment you ran the query. If you run the same query with the same data a week later, the result will be different because the reference point `now` has moved.

## Allen's Interval Relations

Built-in predicates for comparing intervals (based on Allen's interval algebra):

| Predicate | Meaning |
|-----------|---------|
| `:interval:before(T1, T2)` | T1 ends before T2 starts |
| `:interval:after(T1, T2)` | T1 starts after T2 ends |
| `:interval:meets(T1, T2)` | T1 ends exactly when T2 starts |
| `:interval:overlaps(T1, T2)` | T1 and T2 share some time |
| `:interval:during(T1, T2)` | T1 is contained within T2 |
| `:interval:contains(T1, T2)` | T1 contains T2 |
| `:interval:starts(T1, T2)` | T1 and T2 start together |
| `:interval:finishes(T1, T2)` | T1 and T2 end together |
| `:interval:equals(T1, T2)` | T1 and T2 are identical |

## Interval Functions

Extract components from bound interval variables:

| Function | Returns |
|----------|---------|
| `fn:interval:start(T)` | Start time in nanoseconds |
| `fn:interval:end(T)` | End time in nanoseconds |
| `fn:interval:duration(T)` | Duration in nanoseconds |

Example:
```
# Get the duration of an event
event_duration(X, D) :-
    event(X)@[S, E],
    D = fn:time:sub(E, S).
```

## Interval Variable Binding

You can bind the interval components of a matching fact to variables:

```
# Bind the validity interval to S and E
event_with_time(X, S, E) :- event(X)@[S, E].

# Shorthand: Bind both start and end to the same variable T (point interval)
point_event(X, T) :- event(X)@[T].
```

The bound variables are timestamps in nanoseconds.

## Interval Coalescing

When facts have adjacent or overlapping intervals, they get merged:

```
# If you assert:
employed(/alice)@[2020-01-01, 2021-12-31].
employed(/alice)@[2022-01-01, 2023-12-31].

# Coalescing produces:
employed(/alice)@[2020-01-01, 2023-12-31].
```

This prevents interval explosion in recursive rules. Coalescing works at **nanosecond precision**, meaning it correctly merges intervals regardless of whether they represent days, hours, seconds, or even smaller units. Two intervals are considered adjacent if there is no gap (or exactly 1 nanosecond gap) between them.

## Temporal Declarations

Mark a predicate as temporal using the `temporal` keyword in declarations:

```
# Declare a temporal predicate
Decl employee_status(person, status) temporal bound [/name, /string].

# Regular (eternal) predicate for comparison
Decl config_setting(key, value) bound [/string, /string].
```

The `temporal` keyword signals that facts for this predicate have validity
intervals. You can check if a declaration is temporal programmatically:

```go
if decl.IsTemporal() {
    // This predicate has temporal semantics
}
```

> [!IMPORTANT]
> If a predicate is declared `temporal`, **all** its facts and rules must have a temporal annotation (`@[...]`). Unannotated facts are not allowed for temporal predicates. Conversely,non-temporal predicates cannot have temporal annotations.

## Example: Checking Certification Compliance

Here's a realistic use case - make sure operators had certifications before
using equipment:

```
# Declare predicates
Decl certified(person, cert) temporal.
Decl operated(person, equipment, timestamp) temporal.

# Facts
certified(/alice, /forklift)@[2023-01-01, 2024-01-01].
operated(/alice, /forklift, _)@[2023-06-15].

# Rule: Find violations - operated without 30 days of certification
violation(Person, Equipment) :-
    operated(Person, Equipment, _)@[Time, Time],
    ![-[30d, 30d] certified(Person, Equipment).
```

## Programmatic Usage

To use temporal features from Go:

```go
import (
    "time"
    "codeberg.org/TauCeti/mangle-go/engine"
    "codeberg.org/TauCeti/mangle-go/factstore"
)

// Create a temporal store and add facts
store := factstore.NewTemporalStore()
store.Add(myAtom, interval)

// Evaluate with temporal support
stats, err := engine.EvalProgramWithStats(
    programInfo,
    regularStore,
    engine.WithTemporalStore(store),
    engine.WithEvaluationTime(time.Now()),
)
```

### Temporal Store API

The `TemporalFactStore` interface provides these methods:

```go
// Add a temporal fact (returns added, error)
store.Add(atom ast.Atom, interval ast.Interval) (bool, error)

// Add a fact that's always true
store.AddEternal(atom ast.Atom) (bool, error)

// Query facts valid at a specific time
store.GetFactsAt(query ast.Atom, t time.Time, callback) error

// Query facts overlapping an interval
store.GetFactsDuring(query ast.Atom, interval ast.Interval, callback) error

// Merge adjacent/overlapping intervals
store.Coalesce(predicate ast.PredicateSym) error
```

### Time and Interval Helpers

The `ast` package provides convenience functions to reduce verbosity when creating times and intervals:

```go
// Create dates without typing all the zeros
t := ast.Date(2024, 1, 15)                    // midnight in default timezone
t := ast.DateTime(2024, 1, 15, 10, 30)        // with hour and minute
t := ast.DateTimeSec(2024, 1, 15, 10, 30, 45) // with seconds

// Create intervals concisely
interval := ast.TimeInterval(startTime, endTime)
interval := ast.DateInterval(2023, 1, 1, 2024, 12, 31)  // most concise
```

**Before** (verbose):
```go
store.Add(atom, ast.NewInterval(
    ast.NewTimestampBound(time.Date(2023, 1, 1, 0, 0, 0, 0, time.UTC)),
    ast.NewTimestampBound(time.Date(2024, 12, 31, 0, 0, 0, 0, time.UTC)),
))
```

**After** (concise):
```go
store.Add(atom, ast.DateInterval(2023, 1, 1, 2024, 12, 31))
```

| Helper | Example | Purpose |
|--------|---------|---------|
| `ast.Date(y, m, d)` | `ast.Date(2024, 1, 15)` | Date at midnight |
| `ast.DateTime(y, m, d, h, min)` | `ast.DateTime(2024, 1, 15, 10, 30)` | Date with time |
| `ast.DateTimeSec(y, m, d, h, min, s)` | `ast.DateTimeSec(2024, 1, 15, 10, 30, 45)` | Date with seconds |
| `ast.DateIn(y, m, d, tz)` | `ast.DateIn(2024, 1, 15, "PST")` | Date in specific timezone |
| `ast.DateTimeIn(y, m, d, h, min, tz)` | `ast.DateTimeIn(2024, 1, 15, 10, 30, "EST")` | Date+time in specific timezone |
| `ast.TimeInterval(start, end)` | `ast.TimeInterval(t1, t2)` | Interval from time.Time values |
| `ast.DateInterval(...)` | `ast.DateInterval(2023, 1, 1, 2024, 12, 31)` | Interval from date components |

### Timezone Configuration

All date/time helpers use a configurable default timezone (UTC by default). Set it once at program startup:

```go
// Default: UTC (no configuration needed)

ast.SetTimezone("UTC")                   // Explicit UTC
ast.SetTimezone("Local")                 // System timezone
ast.SetTimezone("America/New_York")      // IANA timezone name
ast.SetTimezone("PST")                   // Common abbreviations work too

// For init(), use MustSetTimezone (panics on error)
func init() {
    ast.MustSetTimezone("America/New_York")
}
```

Supported abbreviations: `EST`, `CST`, `MST`, `PST`, `GMT`, `CET`, `JST`, `IST`, and more.

**Important:** Set the timezone once at startup before creating any temporal facts.

For one-off values in a different timezone without changing the default, use `DateIn` or `DateTimeIn`:

```go
// Default is UTC, but this one event is in NYC time
store.Add(event, ast.TimeInterval(
    ast.DateTimeIn(2024, 1, 15, 19, 0, "America/New_York"),  // 7pm NYC
    ast.DateTimeIn(2024, 1, 15, 22, 0, "EST"),               // 10pm EST
))
```

## Time Bridge Functions

When mixing temporal reasoning with regular data columns containing timestamps:

| Function | Purpose |
|----------|---------|
| `fn:time:from_nanos(N)` | Convert nanoseconds to temporal-compatible value |
| `fn:time:to_nanos(T)` | Convert temporal bound to nanoseconds |
| `fn:time:add(T, D)` | Add duration (nanos) to timestamp |

Example:
```
# Bridge between a column timestamp and temporal queries
valid_order(Order) :-
    order(Order, CreatedAtNanos),
    Timestamp = fn:time:from_nanos(CreatedAtNanos),
    fn:time:after(Timestamp, fn:time:add(fn:time:now, -2592000000000000)).  # 30 days in nanos
```

## Decidability and Termination

Temporal reasoning introduces potential non-termination. The implementation includes
safeguards, but understanding safe vs dangerous patterns helps avoid issues.

### Safe Patterns (Guaranteed to Terminate)

```
# SAFE: Past-only lookback, no temporal head
recent_login(User) :-
    <-[7d] login(User).

# SAFE: Temporal head but no recursion through temporal predicates
expires_soon(License) @[now, End] :-
    license(License) @[_, End],
    :interval:before(End, fn:time:add(now, 2592000000000000)).
```

### Dangerous Patterns (May Not Terminate)

```
# DANGEROUS: Recursive temporal derivation with expanding intervals
extended(X) @[T1, T2] :-
    base(X) @[T1, T0],
    extended(X) @[T0, T2].  # Self-reference extends interval

# DANGEROUS: Unbounded future generation
will_happen(X) @[now, _] :-
    trigger(X),
    [+[1d] will_happen(X).  # Infinite future facts
```

### Built-in Safeguards

1. **Interval Coalescing**: Adjacent/overlapping intervals are merged automatically
2. **Interval Limit**: Default 1000 intervals per atom, configurable via `WithMaxIntervalsPerAtom(n)`
3. **Fact Limits**: Use `engine.WithCreatedFactLimit(n)` to cap total derived facts

Configure the interval limit:
```go
// Custom limit
store := factstore.NewTemporalStore(factstore.WithMaxIntervalsPerAtom(5000))

// No limit (use with caution)
store := factstore.NewTemporalStore(factstore.WithMaxIntervalsPerAtom(-1))
```

### Complexity

Based on DatalogMTL research:
- Non-recursive temporal queries: AC⁰ data complexity
- Full DatalogMTL: PSPACE-complete data complexity
- Forward-propagating programs: May not terminate without coalescing