Metadata-Version: 2.4
Name: linear-itertools
Version: 0.1.0
Summary: Lazily enumerate normal-form terms of a linear logic type
Author: Joel Sjogren
License-Expression: MIT
Project-URL: Homepage, https://github.com/joelsjogren/linear-itertools
Keywords: linear logic,lambda calculus,type theory,enumeration
Classifier: Development Status :: 3 - Alpha
Classifier: Intended Audience :: Developers
Classifier: Intended Audience :: Science/Research
Classifier: Topic :: Software Development :: Libraries
Classifier: Topic :: Scientific/Engineering :: Mathematics
Classifier: Programming Language :: Python :: 3
Classifier: Programming Language :: Python :: 3 :: Only
Requires-Python: >=3.9
Description-Content-Type: text/markdown
License-File: LICENSE
Provides-Extra: test
Requires-Dist: pytest; extra == "test"
Dynamic: license-file

# linear-itertools

Lazily enumerate every normal-form term of a type in the multiplicative
fragment of intuitionistic linear logic.

This project was entirely vibe coded.

```python
import linear_itertools as lit

for t in lit.terms("(a -> a) -> (a -> a) -> (a -> a) -> (a -> b) -> (b -> a) -> a -> a"):
    print(t)
```

```
\(f1 : a -> a) -> \(f2 : a -> a) -> \(f3 : a -> a) -> \(f4 : a -> b) -> \(f5 : b -> a) -> \(a1 : a) -> f1 (f2 (f3 (f5 (f4 a1))))
\(f1 : a -> a) -> \(f2 : a -> a) -> \(f3 : a -> a) -> \(f4 : a -> b) -> \(f5 : b -> a) -> \(a1 : a) -> f1 (f2 (f5 (f4 (f3 a1))))
...
```

## Why linear logic?

In ordinary (intuitionistic) logic, `a -> b -> a` has one inhabitant
(`\x y. x`) because a hypothesis may be discarded (weakening) or reused
(contraction). In **linear** logic every hypothesis must be used **exactly
once**, so `a -> b -> a` has *zero* inhabitants (`y` would go unused) and
`a -> a -> a` also has zero (you'd need to use `x` twice). This makes the
set of inhabitants of a fixed type *finite* and enumerable by construction
-- there's no way to pad a term out indefinitely, since nothing can be
discarded or duplicated. That's what makes `lit.terms(...)` a well-defined,
terminating, and typically small (or empty!) enumeration rather than an
unbounded search.

## Type syntax

| Meaning                    | Syntax          | Alt. spelling |
|-----------------------------|-----------------|----------------|
| type variable                | `a`, `b`, `foo`  |                |
| linear implication           | `a -> b`         | `a -o b`       |
| tensor product                | `a * b`          | `a (x) b`      |
| multiplicative unit           | `1`              |                |
| universal quantification      | `forall a b. t`  | `forall a, b. t` |

`->` and `-o` are right-associative; `*` and `(x)` are right-associative
and bind tighter than `->`. Parentheses group as usual. `(x)` as a
standalone atom (not between two types) is read as the variable `x`.

Any type variable left free in a type string is implicitly quantified with
`forall` at the front, in order of first appearance -- so `a -> a` means
`forall a. a -> a`.

`forall` isn't limited to a prenex prefix -- it can appear anywhere a type
can: as an arrow's codomain, as an arrow's *domain* (giving a hypothesis
that's itself polymorphic), inside a tensor component, and so on. It must
be parenthesized except at the very start of a type or immediately after
`->` (where it extends as far right as possible, Haskell-style):

```python
list(lit.terms("(a -> a) -> (a -> a) -> (a -> a) -> (forall b. (a -> a))"))
list(lit.terms("(forall b. b -> b) -> a -> a"))   # a polymorphic hypothesis
```

Using a polymorphic hypothesis (the second example) requires instantiating
its variables, which only has a well-defined answer when they're pinned
down by unifying the tail of its use against the goal (or against a later
argument) -- if a variable is only ever used in argument position with
nothing to pin it down, guessing a type for it would be unsound, so that
path is simply skipped rather than guessed at.

`lit.type(s)` parses a type string on its own, without generating any
terms, and returns it as a `Type` object (a `Forall` scheme). Its `repr`
shows the type printed back in canonical, precedence-resolved form, which
is a quick way to build intuition for the precedence rules -- e.g. redundant
parentheses around a tensor operand disappear, since `*` already binds
tighter than `->`:

```python
>>> lit.type("a -> a -> b")
<Type 'forall a b. a -> a -> b'>
>>> lit.type("(a * b) -> c")
<Type 'forall a b c. a * b -> c'>
>>> lit.type("(a -> a) -> b")
<Type 'forall a b. (a -> a) -> b'>
```

## Terms

Each term produced by `lit.terms(...)` is a `Term`:

- `term.pretty()` (also `str(term)`) -- a human-readable style with
  binder names derived from their type, e.g. `\(a1 : a) -> a1`.
- `term.debruijn()` -- the same term with de Bruijn indices instead of
  names, e.g. `\(a). #0`.
- `term.type_str()` -- the term's type, as a parseable string.
- `term.type` / `term.scheme` -- the type as a `Forall` scheme (the
  structured `Type` AST, not a string).

`lit.terms(...)` itself returns a `Terms` object rather than a plain
generator: it's still lazy and single-pass for `for`/`next()`, but is also
subscriptable for convenience at a REPL, including negative indices and
`len()` (indexing never disturbs where a separate `for`/`next()`
iteration over the same object is at, or vice versa -- forcing enough of
the enumeration to answer an index just fills a shared cache):

```python
>>> ts = lit.terms("(a -> a) -> (a -> a) -> (a -> a) -> (a -> b) -> (b -> a) -> a -> a")
>>> ts[0]
<Term ... >
>>> ts[-1]        # last term -- forces (and caches) the full enumeration
<Term ... >
>>> len(ts)
24
```

## Application

`lit.apply(f, x)` (equivalently `f.apply(x)` or `f(x)`) applies one term
to another. If `f`'s type has `forall`-quantified variables, they are
instantiated automatically by unifying `f`'s domain type against `x`'s
type -- exactly like applying a Haskell polymorphic function, you never
specify the instantiation yourself. This unification is bidirectional: if
`x` itself has its own schema variables, applying `f` can constrain them
too, including unifying two of `x`'s own variables *with each other*:

```python
identity = next(lit.terms("forall a. a -> a"))
swap = next(lit.terms("forall a b. a * b -> b * a"))
pair = next(lit.terms("(e -> e) * 1"))

lit.apply(identity, swap)   # forall a b. a * b -> b * a  (a, b re-instantiated)
lit.apply(swap, pair)       # forall e. 1 * (e -> e)

# back : forall a. (a -> a) -> (a -> a) -> (a -> a) -> a -> a
# flip : forall a b. a * b -> b * a
# back's domain is "T -> T" (same type on both sides), so applying it to
# flip forces flip's own a and b to unify with each other:
back = next(lit.terms("forall a. (a -> a) -> (a -> a) -> (a -> a) -> a -> a"))
flip = next(lit.terms("forall a b. a * b -> b * a"))
lit.apply(back, flip)   # forall b. (b*b -> b*b) -> (b*b -> b*b) -> b*b -> b*b
```

Applying a term whose type isn't `A -> B`, or whose domain doesn't unify
with the argument's type, raises `TypeError`. The result is always itself
a genuine normal form -- `apply()` beta-reduces (and, where needed,
commutes `let`-destructurings past the reduction they were blocking), so
chained application composes as you'd expect:

```python
back = next(lit.terms("forall a. (a -> a) -> (a -> a) -> (a -> a) -> a -> a"))
flip = next(lit.terms("forall a b. a * b -> b * a"))
lit.apply(lit.apply(lit.apply(back, flip), flip), flip)
# \(p1 : b * b) -> let (b1, b2) = p1 in (b2, b1)   -- flip composed with
# itself three times is flip again (flip is an involution), collapsed to
# a single swap, not left as three nested, unreduced applications.
```

## Permutations

`lit.encode_permutation(perm)` and `lit.decode_permutation(term)` convert
between a plain Python permutation (a list where `perm[i]` says which
input position feeds output position `i`) and a `Term` of the type
`a * a * ... * a -> a * a * ... * a` (n copies of `a`, matching
`len(perm)`). Every normal-form term of that type destructures its input
tuple and repackages the pieces in some order -- linearity guarantees
each piece is used exactly once -- so that order *is* a permutation, and
`lit.terms(...)` on that type enumerates exactly the `n!` of them:

```python
>>> lit.encode_permutation([1, 2, 0]).pretty()
'\\(p1 : a * a * a) -> let (a1, a2) = p1 in let (a3, a4) = a2 in (a3, (a4, a1))'
>>> lit.decode_permutation(lit.encode_permutation([1, 2, 0]))
[1, 2, 0]
```

Composing two such terms (via `apply()`, applying one after the other)
and composing the underlying permutations agree -- `decode_permutation`
turns term composition into permutation composition, an isomorphism
exercised in `tests/test_permutation.py`.

## What "normal form" means here

`lit.terms(...)` enumerates **eta-long, beta-normal** terms: every
subterm of a non-atomic type is fully written out in introduction form
(`\x -> ...` for function types, `(m, n)` for tensor types), and only
atomic-typed positions may be a "neutral" elimination spine
(`h m1 m2 ...`, possibly interleaved with `let (x, y) = ... in` /
`let () = ... in` destructuring). Terms that are related only by
*commuting conversions* -- e.g. reordering two independent `let`
destructurings of unrelated hypotheses -- are **not** separately
enumerated; one canonical ordering is picked. This keeps the enumeration
free of uninteresting combinatorial duplicates while still enumerating
every essentially distinct proof/term.

## Status

Early / alpha. The core enumeration, printing, and application are
implemented and tested; API details may still change before the first
PyPI release.
