Command-Line Manipulator of 𝜑-Calculus Expressions

This is a command-line normalizer, rewriter, and dataizer of 𝜑-calculus expressions.

First, you write a simple 𝜑-calculus expression in the hello.phi file:

⟦ φ ↦ ⟦ Δ ⤍ 68-65-6C-6C-6F ⟧, t ↦ ξ.k, k ↦ ⟦⟧ ⟧

Installation

Then you can install phino in two ways:

Install Cabal first and then:

cabal update
cabal install --overwrite-policy=always phino-0.0.134
phino --version

Or download binary from the internet using curl or wget:

sudo curl -o /usr/local/bin/phino http://phino.objectionary.com/releases/macos-15/phino-latest
sudo chmod +x /usr/local/bin/phino
phino --version

Download paths are:

• Ubuntu 22.04: http://phino.objectionary.com/releases/ubuntu-22.04/phino-latest
• Ubuntu 24.04: http://phino.objectionary.com/releases/ubuntu-24.04/phino-latest
• MacOS (ARM): http://phino.objectionary.com/releases/macos-15/phino-latest
• MacOS (Intel): http://phino.objectionary.com/releases/macos-14-large/phino-latest
• Windows: http://phino.objectionary.com/releases/windows-2022/phino-latest.exe

Build

To build phino from source, clone this repository:

git clone git@github.com:objectionary/phino.git
cd phino

Then, run the following command (ensure you have Cabal installed):

cabal build all

Next, run this command to install phino system-wide:

sudo cp "$(cabal list-bin phino)" /usr/local/bin/phino

Verify that phino is installed correctly:

$ phino --version
0.0.0

You can ensure scripts are run with a specific version of phino using the --pin global option. It exits with an error when the version supplied doesn't match the installed one:

phino --pin=0.0.0.67 dataize hello.phi

Dataize

Then, you dataize the expression:

$ phino dataize hello.phi
68-65-6C-6C-6F

Symbolic λ functions

Which λ functions exist is a property of the object model being dataized, not of the calculus, so phino implements none of them. They come from a YAML file given with --symbolic, one entry per λ function:

- λ: L_number_(plus|times)
  dataize:
    𝛿1: $.ρ
    𝛿2: $.x
  𝑛: Φ.number( φ ↦ ⟦ λ ⤍ 𝜎 ⟧ )

The λ of an entry is the λ names it answers for, as a regular expression, so the one above stands for L_number_plus and L_number_times. Under dataize stand the operands it brings down to data through 𝔻, each binding a bytes meta 𝛿1, 𝛿2 and so on; under morph the operands it reduces to a normal form through 𝕄, each binding an expression meta 𝑛1, 𝑛2. Both blocks are terms of the calculus, read against the formation being fired, so ξ is that formation and $.x its x, while Φ is the universe. Every entry numbers its own metas from 𝛿1 and 𝑛1, and the entry is what tells two 𝛿1 apart.

The term under 𝑛 is what the firing answers with. phino normalizes it exactly as it normalizes anything else, so --protocol, --partial and --max-steps work on it unchanged. It may name any meta the entry bound, those of the two blocks below among them.

Standing data into unknowns

There is a third block, symbolize, and it reduces nothing. It takes a term another meta of the entry is already bound to and binds an expression meta of its own to that same term with every datum in it standing for an unknown:

- λ: L_fork
  dataize:
    𝛿1: $.φ
  morph:
    𝑛1: $.left
    𝑛2: $.right
  symbolize:
    𝑛3: 𝑛1
    𝑛4: 𝑛2
  𝑛: 𝑛3

The right-hand side of a line names a meta bound by morph or by a symbolize line above it, and nothing else; a term nobody reduced has no data to stand. Every Δ ⤍ b binding of that term becomes a λ ⤍ 𝜎k naming a fresh symbol, one per occurrence, so ⟦ Δ ⤍ b ⟧ reads as ⟦ λ ⤍ 𝜎k ⟧ and a literal tuple gets several. A term carrying no datum passes through as it was.

Only the φ chain is walked. A term carries the value it stands for where that chain ends, so a datum standing anywhere else says nothing about the term and is left alone, the whole subtree of it. What sits under ρ belongs to the object around this one, and a normal form drags the universe it was reduced inside along under ρ, so a walk reaching into it would stand the data of the whole program into unknowns to say one thing about one term. What sits under a method is code and not data: the -1 of a neg ↦ ⟦ φ ↦ ξ.ρ.times( -1 ) ⟧ nobody has called is the body of a method, and minting a symbol for it, and for every other literal every method of the carrier declares, would write unknowns nobody ever reads.

This is what lets an entry compare two branches of a fork. A literal is sugar for Φ.number( Φ.bytes( ⟦ Δ ⤍ … ⟧ ) ), so a branch computed from a literal keeps a datum three levels down where a branch computed from an unknown keeps ⟦ λ ⤍ 𝜎 ⟧. A Δ against a λ is a difference in kind and not in value, and after the stage both branches carry ⟦ λ ⤍ 𝜎 ⟧ where they differ.

Joining the branches of a fork

A branching λ function answers neither of its branches. Which one the program takes is decided by a value nobody worked out, so handing one of them through would drop the branch point from the program altogether and a reader would see the condition computed and thrown away. join is the fourth block, and it reduces nothing either: it takes two metas the entry has bound already and binds one of its own to the two terms joined into one.

- λ: L_fork
  dataize:
    𝛿1: $.φ
  morph:
    𝑛1: $.left
    𝑛2: $.right
  symbolize:
    𝑛3: 𝑛1
    𝑛4: 𝑛2
  join:
    𝑛5: [𝑛3, 𝑛4]
  𝑛: 𝑛5

A line names two metas bound by morph, by symbolize or by a join line above it, and never three: it stands for a choice between two branches, and a walk over three terms in parallel is no such choice. The meta it binds is one like any other, so the answer may name it alone, as above, or stand it inside a larger term.

phino takes the two terms and requires them to match verbatim, with one exception: where ⟦ λ ⤍ 𝜎A ⟧ in one meets a different ⟦ λ ⤍ 𝜎B ⟧ in the other, it mints a fresh 𝜎C and stands it there. The same symbol on both sides stays as it is, and the same pair met again further down gets the same fresh symbol, since it is one choice however often the two terms differ by it; two different pairs get two fresh symbols. Two identical terms join into that same term and nothing is minted at all. The join keeps the type by construction, being the terms' own shape, so the file needs to know nothing about carriers.

Only the φ chain is compared, exactly as symbolize stands only that chain into unknowns: a term carries the value it stands for where its φ chain ends, so every other binding is taken from the first branch, the whole subtree of it, and never compared at all. The two branches of a fork reach their normal forms in scopes of their own, so their ρ differ wherever the reduction left a trace, and comparing them would refuse the join over something saying nothing about either branch; a method is the same, its body being code nobody has called, so two branches differing inside one are not two values. The joined term keeps the methods and the ρ of the first of the two, being of its shape, which is what lets the program go on dispatching on what the fork answered.

A join is only ever between two expressions and a datum is never joined with anything, which is why symbolize runs before it: a known symbol, one that stage minted for a datum, is a symbol like any other here, so a literal branch joins with a computed one and two literal branches join too. Any other difference — a datum against a symbol, two different data, a binding one term carries and the other does not — is no join at all, and the firing gets stuck the way a λ function no entry answers does, so --partial parks it rather than aborting the run. A fork whose branches differ in structure, such as a Φ.true and a Φ.false written as φ ↦ ξ.left against φ ↦ ξ.right, is stuck, and bringing two such branches to one shape is the program's job and not phino's.

Every symbol a join mints is written into the protocol as a fact of its own, so a reader ties it to the two it stands for without diffing the terms; the section on --protocol below shows one.

Symbols

An entry answers, it never computes. The job of these functions is symbolic morphing: what 5.plus( 6 ) comes to is the arithmetic of the object model and not phino's, so an entry answers a term carrying a symbol standing for a value nobody worked out, and the data its dataize operands came down to is not its to read. An answer mentioning a 𝛿 is refused where the file is read.

𝜎 is a meta of the calculus, beside 𝑛, 𝛿 and 𝑓, and it stands where a λ name stands. In a term, 𝜎1 is a concrete symbol: a λ function nothing answers, which is what makes the value the term carries unknown. Firing it is therefore the same question as firing a λ name the --symbolic file does not carry, and gets the same answer: 𝔼 stops there, the protocol records the site as ?(𝜎1), and --partial leaves the term where it stands. Dispatching an attribute off a symbol — ⟦ λ ⤍ 𝜎1 ⟧.plus( 5 ) — therefore taints its own binding and nothing else; what stands beside it still computes. In an answer, a bare 𝜎 asks for a fresh one, minted as the firing happens and numbered by the run, so no two unknowns are ever spelled alike. Minting starts after the symbols the program already carries, so a run over the 𝜑-program an earlier run wrote never spells a fresh symbol like one already standing there.

Dataizing a symbol never gets stuck. It answers a fixed datum, 42 (40-45-00-00-00-00-00-00), the same one for every symbol, so 𝔻 always answers, a 𝛿 always holds concrete data and no firing ever declines for the lack of it:

$ cat sum.phi
⟦
  bytes ↦ ⟦ φ ↦ ∅ ⟧,
  number ↦ ⟦ φ ↦ ∅, plus(x) ↦ ⟦ λ ⤍ L_number_plus ⟧ ⟧,
  φ ↦ 5.plus( 6 )
⟧
$ phino dataize --symbolic=atoms.yaml --sweet --hide-rho sum.phi
40-45-00-00-00-00-00-00

The keys of the file

Each λ is a regular expression, and it must match the whole λ name, so a plain name such as L_number_plus means that one function and nothing else, while L_number_.* stands for every function of number. The keys are unique: nothing tells two entries under one key apart, so a second entry under a key is unreachable and the file is refused rather than merely redundant.

A λ name no key matches has no λ function at all, so 𝔼 gets stuck on it. Without --symbolic there is no entry at all and every λ function gets stuck:

$ phino dataize --sweet --hide-rho sum.phi
[ERROR]: No entry of --symbolic answers the λ function 'L_number_plus'

The file is read before anything is parsed or reduced, so a key that is no regular expression, an operand that is no meta of the kind its block binds, or an answer the calculus cannot read fails the run up front rather than half-way through a derivation.

Recording what fired

Every λ function fired on the way to the answer may be recorded in a machine-readable protocol, with the --protocol option. The protocol is a tree: the run at the top, one block per firing under it, and inside the block the operands the firing bound and the term it answered with.

$ phino dataize --symbolic=atoms.yaml --protocol=atoms.txt --quiet \
    --sweet --hide-rho sum.phi
$ cat atoms.txt
𝔻(Φ)
  𝔼(L_number_plus)  # 𝔻(Φ)
    𝛿1.1 := 40-14-00-00-00-00-00-00  # 𝔻(ξ.ρ)
    𝛿2.1 := 40-18-00-00-00-00-00-00  # 𝔻(ξ.x)
    𝑛.1.1 := Φ.number( φ ↦ ⟦ λ ⤍ 𝜎1 ⟧ )  # 𝑛
    𝑛.1.2 := ⟦ φ ↦ ⟦ λ ⤍ 𝜎1 ⟧, plus(x) ↦ ⟦ λ ⤍ L_number_plus ⟧ ⟧  # 𝕄(𝑛.1.1)

𝔻(…) is the run and the term it was aimed at, 𝕄(…) where the run is a morphing, and 𝔼(…) is one firing, named by the entry that answered it and commented with the judgment that asked for it and the site it was fired at. Every comment of the file is of that shape: a judgment applied to a term, which is the intent the value beside it came from. The firings are numbered across the whole run, in the order they open, so 𝛿1.2 is the value bound to 𝛿1 by the second firing of the run, whichever λ function that was, 𝑛1.2 the same for a morph meta, and 𝑛.3.2 the answer of the third firing, so 𝑛1.2 := 𝑛.3.2 reads "the 𝑛1 of this firing is what the third firing answered". One firing binds a meta once and no two firings share a number, so every one of these names stands on exactly one line of the file and a line naming another one points at it and no other.

An answer stands on two lines and not one. A firing answers the term its entry wrote and phino morphs that term before standing it back into the program, so 𝑛.1.1 is what the entry wrote, with the symbols this firing minted already in it, commented with 𝑛 to name the key it was read from, and 𝑛.1.2 is the normal form 𝕄 made of it, commented with 𝕄(𝑛.1.1) to say where it came from. It is the same morphing every other term goes through, and writing only its outcome would have the formation of number appear in place of the three tokens the entry wrote with nothing saying why. Whatever that morphing fires opens its own block between the two lines, exactly where a firing an operand took opens one, so the order the lines come in is the order the work was done in.

Where an operand came down to the datum a symbol stands for, the protocol writes 𝔻(⟦ λ ⤍ 𝜎1 ⟧) in place of that 42, so a reader sees that the value was manufactured rather than read out of the program. A 𝜎 is the name of a λ function and no term of its own, so 𝔻 is applied to the formation carrying it and never to the name alone.

A symbolize line writes a line per fresh symbol it minted, ahead of the line binding the term that carries them, and that line is a fact and no assignment: 𝔻(⟦ λ ⤍ 𝜎44 ⟧) == 3F-F0-00-00-00-00-00-00 says that dataizing the formation 𝜎44 names answers those bytes. Nothing binds bytes to a 𝜎, since it is neither a datum nor a term. A consumer reading the protocol back treats a symbol with such a fact as a constant and every other symbol as an unknown.

The line binding the term of a symbolize one is commented with the meta it was told to stand, 𝑛3.1 := ⟦ λ ⤔ 𝜆8 ⟧ # 𝑛1, and with no judgment around it: standing the data of a term into unknowns is the file's own operation and nothing of the calculus runs there, so the line names a meta of the entry the way a join line names the two it joined. A comment carries the letter of a judgment exactly where a judgment made the value.

The site of a firing is a locator, written as a comment the way an operand line writes the term it came from, under the letter of the judgment that asked for the firing: 𝔼 is fired by the ml rule of morphing and by the fire rule of dataization, so 𝕄(Φ.demo.a.φ) is a λ function fired while 𝕄 was reducing that binding and 𝔻(Φ) one fired because dataization demanded data of Φ. A chain such as 5.plus( 6 ).plus( 7 ) writes both: the inner call is fired while 𝕄 reduces the head of the outer dispatch, the outer one because 𝔻 asked for the data. The site itself is where in the program the firing belongs: the term the run was aimed at, so Φ for a run that was aimed at nothing in particular, and, under --deep, the binding the walk had entered when the λ function fired, since that walk reduces every part of the program in turn and one entry answers the same way wherever it is fired. A locator names a binding and reaches no further, so a firing standing deeper inside a term than that — under a dispatch, or in the argument of an application — is written under the last binding the walk entered, which is the smallest part of the program a reader can aim a run of their own at. An operand of a firing is reduced bound to a synthetic attribute of the universe (see --inside below), so a λ function fired while it came down is written under that attribute and not under the site of the firing that asked for it.

An operand line ends in the judgment that reduced it and the term it was reduced from, written as a comment after two spaces and #. The value alone says what the meta was bound to and neither what it was bound from nor what was done to it, so 𝛿1.1 := 40-14-00-00-00-00-00-00 # 𝔻(ξ.ρ) reads "the 𝛿1 of this firing is the ρ of the formation brought down through 𝔻, and it came down to 20", where a morph operand reads 𝑛1.5 := 𝑛.3.2 # 𝕄(ξ.then) and says that the then of the formation reached its normal form through 𝕄. Which of the two judgments ran is the whole difference between a line ending in data and one ending in a term. It is the very term the entry wrote under that meta, spelled the way the calculus reads it — $ is read as ξ — so a reader never has to open the --symbolic file beside the protocol and match every line by λ name and meta number.

?(…) is a λ name no entry answers, standing where the block of its firing would have stood. Nothing fired, so nothing opens under it. The line is commented with the judgment that asked and the formation it was asking about, 𝕄(⟦ λ ⤍ L_none ⟧), the way an operand line is commented with the term it was reduced from: 𝔼 is fired by the ml rule of morphing and by the fire rule of dataization, so the letter says where in the reduction the site stands and the term says which object the λ function that could not fire belongs to. It is written whether or not --partial goes on to park the run, since the protocol records what 𝔼 was asked for, and a question it could not answer belongs there as much as one it could — once per site and not once per attempt, since a site --partial parks stays in the residue and --deep walks over it again:

$ phino dataize --symbolic=atoms.yaml --protocol=atoms.txt --quiet \
    --sweet --hide-rho stuck.phi
[ERROR]: No entry of --symbolic answers the λ function 'L_number_nope'
$ cat atoms.txt
𝔻(Φ)
  𝔼(L_number_plus)  # 𝕄(Φ)
    𝛿1.1 := 40-14-00-00-00-00-00-00  # 𝔻(ξ.ρ)
    𝛿2.1 := 40-18-00-00-00-00-00-00  # 𝔻(ξ.x)
    𝑛.1.1 := Φ.number( φ ↦ ⟦ λ ⤍ 𝜎1 ⟧ )  # 𝑛
    𝑛.1.2 := ⟦ φ ↦ ⟦ λ ⤍ 𝜎1 ⟧, plus(x) ↦ ⟦ λ ⤍ L_number_plus ⟧, nope ↦ ⟦ λ ⤍ L_number_nope ⟧ ⟧  # 𝕄(𝑛.1.1)
  ?(L_number_nope)  # 𝔻(⟦ λ ⤍ L_number_nope ⟧)

The very same file comes back with --partial, where the run answers the residue instead of failing: what phino could not decide is a property of the program and not of the option that decides what to do about it.

Every term is 𝜑 on a single line, whatever --output and --flat say about the result of the run, so a program reading the protocol back never has to know what the run printed. The file is truncated at the beginning of every run, so it always holds the firings of exactly one run.

The blocks come in the order the reduction walks the term, and that order is not what the dependencies are read from — the symbols are. Take a comparison nobody can decide, a fork branching on it, and an atoms.yaml of three entries, the λ functions named briefly to keep the lines below short:

- λ: L_plus
  dataize:
    𝛿1: $.ρ
    𝛿2: $.x
  𝑛: Φ.number( φ ↦ ⟦ λ ⤍ 𝜎 ⟧ )
- λ: L_gt
  dataize:
    𝛿1: $.ρ
    𝛿2: $.x
  𝑛: Φ.bool( if ↦ ⟦ λ ⤍ L_fork, then ↦ ∅, else ↦ ∅, φ ↦ ⟦ λ ⤍ 𝜎 ⟧ ⟧ )
- λ: L_fork
  dataize:
    𝛿1: $.φ
  morph:
    𝑛1: $.then
    𝑛2: $.else
  join:
    𝑛3: [𝑛1, 𝑛2]
  𝑛: 𝑛3

$ cat fork.phi
⟦
  bytes ↦ ⟦ φ ↦ ∅ ⟧,
  bool ↦ ⟦ if ↦ ∅ ⟧,
  number ↦ ⟦ φ ↦ ∅, plus(x) ↦ ⟦ λ ⤍ L_plus ⟧, gt(x) ↦ ⟦ λ ⤍ L_gt ⟧ ⟧,
  foo(x) ↦ ⟦
    φ ↦ ξ.x.gt( 0 ).if( ξ.x.plus( ξ.x.plus( 1 ) ), ξ.x.plus( ξ.x ) ).plus( 5 )
  ⟧,
  demo ↦ ⟦ a ↦ Φ.foo( Φ.number( φ ↦ ⟦ λ ⤍ 𝜎1 ⟧ ) ) ⟧
⟧
$ phino morph --deep --symbolic=atoms.yaml --locator=Q.demo.a \
    --protocol=fork.txt --quiet --sweet --hide-rho fork.phi
$ cat fork.txt
𝕄(Φ.demo.a)
  𝔼(L_gt)  # 𝕄(Φ.demo.a.φ)
    𝛿1.1 := 𝔻(⟦ λ ⤍ 𝜎1 ⟧)  # 𝔻(ξ.ρ)
    𝛿2.1 := 00-00-00-00-00-00-00-00  # 𝔻(ξ.x)
    𝑛.1.1 := Φ.bool( if ↦ ⟦ λ ⤍ L_fork, then ↦ ∅, else ↦ ∅, φ ↦ ⟦ λ ⤍ 𝜎2 ⟧ ⟧ )  # 𝑛
    𝑛.1.2 := ⟦ if ↦ ⟦ λ ⤍ L_fork, then ↦ ∅, else ↦ ∅, φ ↦ ⟦ λ ⤍ 𝜎2 ⟧ ⟧ ⟧  # 𝕄(𝑛.1.1)
  𝔼(L_plus)  # 𝕄(Φ.demo.a.φ)
    𝛿1.2 := 𝔻(⟦ λ ⤍ 𝜎1 ⟧)  # 𝔻(ξ.ρ)
    𝛿2.2 := 3F-F0-00-00-00-00-00-00  # 𝔻(ξ.x)
    𝑛.2.1 := Φ.number( φ ↦ ⟦ λ ⤍ 𝜎3 ⟧ )  # 𝑛
    𝑛.2.2 := ⟦ φ ↦ ⟦ λ ⤍ 𝜎3 ⟧, plus(x) ↦ ⟦ λ ⤍ L_plus ⟧, gt(x) ↦ ⟦ λ ⤍ L_gt ⟧ ⟧  # 𝕄(𝑛.2.1)
  𝔼(L_plus)  # 𝕄(Φ.demo.a.φ)
    𝛿1.3 := 𝔻(⟦ λ ⤍ 𝜎1 ⟧)  # 𝔻(ξ.ρ)
    𝛿2.3 := 𝔻(⟦ λ ⤍ 𝜎3 ⟧)  # 𝔻(ξ.x)
    𝑛.3.1 := Φ.number( φ ↦ ⟦ λ ⤍ 𝜎4 ⟧ )  # 𝑛
    𝑛.3.2 := ⟦ φ ↦ ⟦ λ ⤍ 𝜎4 ⟧, plus(x) ↦ ⟦ λ ⤍ L_plus ⟧, gt(x) ↦ ⟦ λ ⤍ L_gt ⟧ ⟧  # 𝕄(𝑛.3.1)
  𝔼(L_plus)  # 𝕄(Φ.demo.a.φ)
    𝛿1.4 := 𝔻(⟦ λ ⤍ 𝜎1 ⟧)  # 𝔻(ξ.ρ)
    𝛿2.4 := 𝔻(⟦ λ ⤍ 𝜎1 ⟧)  # 𝔻(ξ.x)
    𝑛.4.1 := Φ.number( φ ↦ ⟦ λ ⤍ 𝜎5 ⟧ )  # 𝑛
    𝑛.4.2 := ⟦ φ ↦ ⟦ λ ⤍ 𝜎5 ⟧, plus(x) ↦ ⟦ λ ⤍ L_plus ⟧, gt(x) ↦ ⟦ λ ⤍ L_gt ⟧ ⟧  # 𝕄(𝑛.4.1)
  𝔼(L_fork)  # 𝕄(Φ.demo.a.φ)
    𝛿1.5 := 𝔻(⟦ λ ⤍ 𝜎2 ⟧)  # 𝔻(ξ.φ)
    𝑛1.5 := 𝑛.3.2  # 𝕄(ξ.then)
    𝑛2.5 := 𝑛.4.2  # 𝕄(ξ.else)
    𝔻(⟦ λ ⤍ 𝜎6 ⟧) ∈ { 𝔻(⟦ λ ⤍ 𝜎4 ⟧), 𝔻(⟦ λ ⤍ 𝜎5 ⟧) }
    𝑛3.5 := ⟦ φ ↦ ⟦ λ ⤍ 𝜎6 ⟧, plus(x) ↦ ⟦ λ ⤍ L_plus ⟧, gt(x) ↦ ⟦ λ ⤍ L_gt ⟧ ⟧  # [𝑛1, 𝑛2]
    𝑛.5.1 := 𝑛3.5  # 𝑛
    𝑛.5.2 := 𝑛3.5  # 𝕄(𝑛.5.1)
  𝔼(L_plus)  # 𝕄(Φ.demo.a.φ)
    𝛿1.6 := 𝔻(⟦ λ ⤍ 𝜎6 ⟧)  # 𝔻(ξ.ρ)
    𝛿2.6 := 40-14-00-00-00-00-00-00  # 𝔻(ξ.x)
    𝑛.6.1 := Φ.number( φ ↦ ⟦ λ ⤍ 𝜎7 ⟧ )  # 𝑛
    𝑛.6.2 := ⟦ φ ↦ ⟦ λ ⤍ 𝜎7 ⟧, plus(x) ↦ ⟦ λ ⤍ L_plus ⟧, gt(x) ↦ ⟦ λ ⤍ L_gt ⟧ ⟧  # 𝕄(𝑛.6.1)

𝜎3 is minted by the second firing and consumed by the third as 𝔻(⟦ λ ⤍ 𝜎3 ⟧), and 𝜎2 by the first and consumed by the fork. 𝜎4 and 𝜎5 are what the two branches came to, and the fork consumes both: its join line makes them one term carrying 𝜎6, which the plus( 5 ) standing after the fork then reads as 𝔻(⟦ λ ⤍ 𝜎6 ⟧). The line 𝔻(⟦ λ ⤍ 𝜎6 ⟧) ∈ { 𝔻(⟦ λ ⤍ 𝜎4 ⟧), 𝔻(⟦ λ ⤍ 𝜎5 ⟧) } is what ties the three together: dataizing the formation 𝜎6 names answers what dataizing one of the other two answers. A reader who knows the entry knows that 𝛿1 is what decides between them and that the first of the two belongs to then. Nothing is assigned to a 𝜎, it being the name of a λ function, so the fact stands on a line of its own the way what a symbolize line knows does, and the line under it binds the meta, commented with the two metas it joined.

Were the fork to answer one of its branches instead, the value of the other would be minted and never consumed, and foo would read as a program that computes a condition, computes both branches and then drops the branch point.

All six firings stand under Φ.demo.a.φ, which is as near as a locator gets to any of them: the walk entered the φ of the formation Φ.demo.a morphs to, and everything under it — the dispatches of the chain, the arguments of if — stands under no attribute of any formation, so the binding the walk had entered is what the protocol writes them under.

A firing that happened while an operand of another was being reduced stands one level deeper, under the firing that asked for it. Here it never happens, because deep morphing reduces both branches where they sit as arguments of if, long before the dispatch that fires the fork.

The protocol as XML

The name of the file decides which of the two formats --protocol writes: a name ending in .xml gets the same tree as markup, every other name gets the indented text above. There is no option for it, since a caller who asks for a file called atoms.xml and gets text back has been told nothing useful. Here is the run at the top of this section again:

$ phino dataize --symbolic=atoms.yaml --protocol=atoms.xml --quiet \
    --sweet --hide-rho sum.phi
$ cat atoms.xml
<?xml version="1.0" encoding="UTF-8"?>
<dataize locator="Φ">
  <evaluate λ="L_number_plus" id="1" judgment="dataize" locator="Φ">
    <bind meta="𝛿1.1">40-14-00-00-00-00-00-00</bind>
    <bind meta="𝛿2.1">40-18-00-00-00-00-00-00</bind>
    <minted>𝜎1</minted>
    <built meta="𝑛.1.1">Φ.number( φ ↦ ⟦ λ ⤍ 𝜎1 ⟧ )</built>
    <answer meta="𝑛.1.2">⟦ φ ↦ ⟦ λ ⤍ 𝜎1 ⟧, plus(x) ↦ ⟦ λ ⤍ L_number_plus ⟧ ⟧</answer>
  </evaluate>
</dataize>

The root is the run itself, named after the judgment it ran — <dataize> for a 𝔻, <morph> for a 𝕄 — with locator naming the term it was aimed at, which is what the text format opens with as 𝔻(Φ). <evaluate> is one firing of 𝔼, λ naming the entry that answered it, id numbering it within the run, judgment naming the one that asked for the firing — the same word the root and a <stuck> carry — and locator naming the site it was fired at. The text format writes those two as the comment of its line, 𝔻(Φ). <bind> is one meta the firing bound, meta naming it the same way the text format names it, counter and all, and the element holding the value it took: a term where the operand was reduced with 𝕄, the datum itself where a dataize operand came down to data. <dataize> inside a firing is the other thing a dataize operand may come to, the datum manufactured for an unknown, and holds the formation that unknown names rather than the 42 standing for it: a 𝜎 is the name of a λ function and no term of its own, so what 𝔻 was applied to is ⟦ λ ⤍ 𝜎2 ⟧ and never 𝜎2 alone. It carries meta where the root carries locator, the same difference the text format draws between 𝔻(Φ) at the top and 𝛿1.2 := 𝔻(…) in a block. The name of the element is what tells a manufactured datum from data, the way 𝔻(…) does in the text format, so nothing has to be read off the presence of an attribute. <answer> holds the term the firing answered with, named the same way by its own meta, and <built> before it holds the term the entry wrote, the one 𝕄 made that answer of: two elements rather than two attributes of one, for the same reason <dataize> is no <bind>.

<known symbol="𝜎44">3F-F0-00-00-00-00-00-00</known> is the fact a symbolize line writes about a symbol it minted, which the text format writes as 𝔻(⟦ λ ⤍ 𝜎44 ⟧) == …: the symbol stands in the attribute a reader joins lines on and the data dataizing its formation answers are the text of the element. It takes symbol and not meta, since the fact is about the unknown and not about a meta the firing bound.

<joined symbol="𝜎6">𝜎4 𝜎5</joined> is the same kind of fact about a symbol a join line minted, which the text format writes as 𝔻(⟦ λ ⤍ 𝜎6 ⟧) ∈ { 𝔻(⟦ λ ⤍ 𝜎4 ⟧), 𝔻(⟦ λ ⤍ 𝜎5 ⟧) }: the fresh symbol stands in symbol and the two it was minted for are the text, in the order the line listed the metas it joined. A line whose two terms differ at several places writes one element per pair of symbols, and one whose terms are alike writes none. The meta the line binds is a <bind> like every other meta of the firing.

<minted>𝜎1</minted> is one symbol the firing minted, one element per bare 𝜎 the entry wrote its answer with, standing inside the block ahead of the <built> carrying them. That is the edge a reader joins on: a later <dataize meta="𝛿1.5">⟦ λ ⤍ 𝜎2 ⟧</dataize> names the symbol the firing that wrote <minted>𝜎2</minted> handed out. A firing minting two symbols writes two elements and one minting none writes none, which no attribute on the answer could say: a term may carry several symbols, or carry one where the value it stands for is not a symbol at all. In the fork above, 𝔼(L_gt) writes <minted>𝜎2</minted> although 𝜎2 sits under if and not where the value of the term is, while 𝔼(L_fork) writes none at all, since the symbol it answers with comes from a join line and stands in a <joined> of its own.

A λ name no entry answers is <stuck λ="…">, standing where its <evaluate> would have stood with the formation 𝔼 was fired against as its text and the judgment that asked in its judgment attribute, where the text format writes the letter of it. A firing that happened while an operand of another was being reduced is an <evaluate> inside the one that asked, which is what the deeper indentation means in the text. Elements are written as the run goes and the open ones are closed when it ends, so a run that fails still leaves a well-formed document behind:

$ phino dataize --symbolic=atoms.yaml --protocol=atoms.xml --quiet \
    --sweet --hide-rho stuck.phi
[ERROR]: No entry of --symbolic answers the λ function 'L_number_nope'
$ cat atoms.xml
<?xml version="1.0" encoding="UTF-8"?>
<dataize locator="Φ">
  <evaluate λ="L_number_plus" id="1" judgment="morph" locator="Φ">
    <bind meta="𝛿1.1">40-14-00-00-00-00-00-00</bind>
    <bind meta="𝛿2.1">40-18-00-00-00-00-00-00</bind>
    <minted>𝜎1</minted>
    <built meta="𝑛.1.1">Φ.number( φ ↦ ⟦ λ ⤍ 𝜎1 ⟧ )</built>
    <answer meta="𝑛.1.2">⟦ φ ↦ ⟦ λ ⤍ 𝜎1 ⟧, plus(x) ↦ ⟦ λ ⤍ L_number_plus ⟧, nope ↦ ⟦ λ ⤍ L_number_nope ⟧ ⟧</answer>
  </evaluate>
  <stuck λ="L_number_nope" judgment="dataize">⟦ λ ⤍ L_number_nope ⟧</stuck>
</dataize>

Reducing a term inside a universe

A term that is no part of the program may still be reduced against it, with the --inside option: the expression it names is bound to a synthetic attribute prepended to the input expression, which the run takes as the universe Φ, normalized there and then reduced.

$ cat universe.phi
⟦
  bytes ↦ ⟦ φ ↦ ∅ ⟧,
  number ↦ ⟦ φ ↦ ∅, plus(x) ↦ ⟦ λ ⤍ L_number_plus ⟧ ⟧
⟧
$ phino dataize --symbolic=atoms.yaml --inside='5.plus( 6 )' universe.phi
40-45-00-00-00-00-00-00

This is the very trick phino plays internally to reduce the operands of a firing, made available to whoever asks it to reduce a term the program does not hold. The option cannot be combined with --locator, since it aims the run at the binding it mints itself. Both dataize and morph take --symbolic and --inside.

Partial evaluation

A λ function no entry of the --symbolic file answers fails the run. This is what happens when an operation is deliberately left out — an input the object model has not declared yet, or an operation whose answer is not known. With --partial, dataization becomes partial evaluation instead: what the known inputs decide is computed, the rest survives as the residual program, which is printed in place of the bytes, and the run ends successfully:

$ cat partial.phi
⟦
  bytes ↦ ⟦ φ ↦ ∅ ⟧,
  number ↦ ⟦
    φ ↦ ∅,
    plus(x) ↦ ⟦ λ ⤍ L_number_plus ⟧,
    times(x) ↦ ⟦ λ ⤍ L_number_times ⟧,
    as-bool ↦ ⟦ λ ⤍ L_number_as_bool ⟧
  ⟧,
  φ ↦ 2.times( 3 ).plus( 4 ).as-bool
⟧
$ phino dataize --symbolic=atoms.yaml --sweet --hide-rho partial.phi
[ERROR]: No entry of --symbolic answers the λ function 'L_number_as_bool'
$ phino dataize --symbolic=atoms.yaml --partial --sweet --hide-rho partial.phi
⟦ λ ⤍ L_number_as_bool ⟧

Here 2.times( 3 ).plus( 4 ) was answered by the entries the file carries, so it was reduced — the symbol it came to sits in the hidden ρ of the residual program — while as-bool names a λ function no entry answers, so it stays in place as a normal-form subterm. A stuck site opens no block in the --protocol file, since nothing fired there, and stands in it as ?(…):

$ phino dataize --symbolic=atoms.yaml --partial --protocol=atoms.txt --quiet \
    --sweet --hide-rho partial.phi
$ cat atoms.txt
𝔻(Φ)
  𝔼(L_number_times)  # 𝕄(Φ)
    𝛿1.1 := 40-00-00-00-00-00-00-00  # 𝔻(ξ.ρ)
    𝛿2.1 := 40-08-00-00-00-00-00-00  # 𝔻(ξ.x)
    𝑛.1.1 := Φ.number( φ ↦ ⟦ λ ⤍ 𝜎1 ⟧ )  # 𝑛
    𝑛.1.2 := ⟦ φ ↦ ⟦ λ ⤍ 𝜎1 ⟧, plus(x) ↦ ⟦ λ ⤍ L_number_plus ⟧, times(x) ↦ ⟦ λ ⤍ L_number_times ⟧, as-bool ↦ ⟦ λ ⤍ L_number_as_bool ⟧ ⟧  # 𝕄(𝑛.1.1)
  𝔼(L_number_plus)  # 𝕄(Φ)
    𝛿1.2 := 𝔻(⟦ λ ⤍ 𝜎1 ⟧)  # 𝔻(ξ.ρ)
    𝛿2.2 := 40-10-00-00-00-00-00-00  # 𝔻(ξ.x)
    𝑛.2.1 := Φ.number( φ ↦ ⟦ λ ⤍ 𝜎2 ⟧ )  # 𝑛
    𝑛.2.2 := ⟦ φ ↦ ⟦ λ ⤍ 𝜎2 ⟧, plus(x) ↦ ⟦ λ ⤍ L_number_plus ⟧, times(x) ↦ ⟦ λ ⤍ L_number_times ⟧, as-bool ↦ ⟦ λ ⤍ L_number_as_bool ⟧ ⟧  # 𝕄(𝑛.2.1)
  ?(L_number_as_bool)  # 𝔻(⟦ λ ⤍ L_number_as_bool ⟧)

Evaluation stays demand-driven, as the calculus prescribes: an argument that nothing asked for before the run got stuck is left as it is in the residual program, for the next iteration.

The nested morphing and dataization recursion is bounded by the --max-steps option (default 1000): when the budget is exhausted, the run fails with Dataization did not finish before reaching the limit of steps. This guards against non-terminating terms, which used to loop forever before the bound was introduced:

$ phino dataize --max-steps=50 problem.phi
[ERROR]: Dataization did not finish before reaching the limit of steps: --max-steps=50

Morph

Dataization insists on bytes. Morphing 𝕄 asks a different question: evaluate as far as the object model allows, without demanding data. It resolves Φ against the universe, peels dispatches and applications through normalization, fires whichever λ functions sit under a dispatch, and stops at the first formation it reaches, handing that formation back untouched. The morph command runs 𝕄 on its own:

$ cat two.phi
⟦
  bytes ↦ ⟦ φ ↦ ∅ ⟧,
  number ↦ ⟦ φ ↦ ∅, plus(x) ↦ ⟦ λ ⤍ L_number_plus ⟧ ⟧,
  φ ↦ 5.plus( 6 ).plus( 7 )
⟧
$ phino dataize --symbolic=atoms.yaml --sweet --hide-rho two.phi
40-45-00-00-00-00-00-00
$ phino morph --symbolic=atoms.yaml --locator=Q.φ --sweet --hide-rho two.phi
⟦ x ↦ 7, λ ⤍ L_number_plus ⟧

The inner 5.plus( 6 ) fires, because .plus is dispatched on its result, and the symbol it answered with lands in the ρ hidden by --hide-rho. The outer application is saturated but bare, so 𝕄 returns it and is finished; firing it is dataization's job and takes dataize on to a datum.

The default locator Q morphs the whole top formation, which 𝕄 returns unchanged, so --locator is how one aims 𝕄 at a subterm, exactly as in dataize. Unlike 𝔻, 𝕄 is total: where no formation is reachable the answer is the terminator ⊥, printed rather than reported as a failed run:

$ phino morph --locator=Q.x <<< '⟦ x ↦ ξ ⟧'
⊥

The whole dataize option surface applies unchanged — --symbolic, --inside, --sequence, --headers, --steps-dir, --protocol, --partial, --max-steps, --shuffle/--seed, --output, --focus and the rest.

Deep morphing

𝕄 stops at the first formation it reaches and hands its bindings back as they were written, since firing a bare λ is dataization's job, and dataize follows the one path dataization demands and ends in bytes. What a program holds but nothing demands — the argument of a λ function no entry answers, for one — is therefore reduced by neither. The --deep flag enters it:

$ cat gap.phi
⟦
  bytes ↦ ⟦ φ ↦ ∅ ⟧,
  number ↦ ⟦ φ ↦ ∅, times(x) ↦ ⟦ λ ⤍ L_number_times ⟧ ⟧,
  bar(x) ↦ ⟦ λ ⤍ L_bar ⟧,
  demo ↦ ⟦ foo ↦ ⟦ n ↦ 3, φ ↦ Φ.bar( ξ.n.times( 5 ).times( 7 ) ) ⟧ ⟧
⟧
$ phino morph --symbolic=atoms.yaml --inside='Q.demo.foo' \
    --sweet --hide-rho gap.phi
⟦ n ↦ 3, φ ↦ Φ.bar( n.times( 5 ).times( 7 ) ) ⟧
$ phino morph --deep --symbolic=atoms.yaml --inside='Q.demo.foo' \
    --sweet --hide-rho gap.phi
⟦ n ↦ 3, φ ↦ Φ.bar( ⟦ φ ↦ ⟦ λ ⤍ 𝜎2 ⟧, times(x) ↦ ⟦ λ ⤍ L_number_times ⟧ ⟧ ) ⟧

Every binding of the formation is entered, recursively. 𝕄 is asked about the term standing there and, where it lands on a saturated formation whose λ an entry answers, that λ is fired and 𝕄 is asked about the answer again. A term on whose way a λ function fired is replaced by the answer of the last firing, morphed: an entry answering Φ.number( φ ↦ ⟦ λ ⤍ 𝜎 ⟧ ) stands the formation of number there, the very one the same term written in the program morphs to, so a value that came out of a firing and a value that was written as a literal are one shape and can be compared leaf by leaf. That costs the size of the object's formation in the residual, which is the price of saying the same thing one way. A term nothing fired on stays exactly as it was written and only its own parts are walked, so Φ.bar keeps its name and what comes back is still the same program, reduced as far as the file allows. The step joins the chain under the name deep, so --sequence shows it, and --max-steps bounds the walk.

Two things are left alone. A λ no entry answers is not fired at all, so --deep stays as total as 𝕄 itself and needs no --partial; a λ function that gets stuck deeper on a spine still fails the run, and --partial parks it, leaving that term as it was written. A firing the walk does make and cannot finish — one whose operand never comes down to data, because a λ nothing answers stands in it — is parked by --partial the same way: the binding it stood in is left as it was written, the walk enters the next one, and the protocol shows the firing with nothing bound under it. One entry nothing can answer therefore taints its own binding and not the whole run. A formation still holding a void binding is not fired either: the void is an argument the program has not given yet, so times(x) ↦ ⟦ λ ⤍ L_number_times ⟧ is a method waiting to be applied, not an application waiting to be computed. Walking the whole program therefore folds what it can and leaves the object model as it was declared:

$ phino morph --deep --symbolic=atoms.yaml --sweet --hide-rho gap.phi
⟦
  bytes(φ) ↦ ⟦⟧,
  number(φ) ↦ ⟦ times(x) ↦ ⟦ λ ⤍ L_number_times ⟧ ⟧,
  bar(x) ↦ ⟦ λ ⤍ L_bar ⟧,
  demo ↦ ⟦
    foo ↦ ⟦
      n ↦ 3,
      φ ↦ Φ.bar( ⟦ φ ↦ ⟦ λ ⤍ 𝜎2 ⟧, times(x) ↦ ⟦ λ ⤍ L_number_times ⟧ ⟧ )
    ⟧
  ⟧
⟧

Acyclic morphing

Whether a program terminates is the object model's business, not the calculus's, so phino prevents no recursion of its own and --max-steps is what ends a run that never finishes. An entry answering with a firing of itself therefore spends the whole budget before it fails, and what it fails on is the limit rather than the loop:

$ cat loop.yaml
- λ: L_loop
  𝑛: ⟦ λ ⤍ L_loop ⟧
$ cat loop.phi
⟦ x ↦ ⟦ λ ⤍ L_loop ⟧.foo ⟧
$ phino morph --symbolic=loop.yaml --locator='Q.x' --max-steps=40 loop.phi
[ERROR]: Dataization did not finish before reaching the limit of steps: --max-steps=40

The --acyclic flag makes a reduction notice. Every frame of 𝕄 and of 𝔻 remembers the terms the frames above it are reducing, and a term that comes back is a question only ever answered by asking it again, so the flag stops there and parks the site the way --partial parks a λ function that cannot fire: the answer is the term the spine had reached, left where it stood, and the command exits successfully.

$ phino morph --symbolic=loop.yaml --locator='Q.x' --acyclic \
    --max-steps=40 --hide-rho loop.phi
⟦ λ ⤍ L_loop ⟧.foo

Each judgment keeps its own memory, since 𝕄 and 𝔻 call each other on the very term they were asked about and that handover is no loop. A body dispatching the object it stands in is one 𝔻 walks round on its own — 𝕄 stops at a formation every round and never sees the same term twice — so dataize takes the flag too, and so does the run of 𝔻 a λ function's dataize operand is brought down with:

$ cat cyc.phi
⟦ cyc ↦ ⟦ x ↦ ∅, φ ↦ Φ.cyc( ξ.x ) ⟧, t ↦ Φ.cyc( ⟦⟧ ) ⟧
$ phino dataize --locator='Q.t' --acyclic --partial \
    --sweet --hide-rho --flat cyc.phi
⟦ cyc(x) ↦ ⟦ φ ↦ Φ.cyc( x ) ⟧, t ↦ ⟦ x ↦ ⟦⟧, φ ↦ Φ.cyc( x ) ⟧ ⟧

𝔻 insists on bytes and a parked term carries none, so under dataize the flag wants --partial to have something to print: the residual program, exactly the one it prints for a λ function that cannot fire. Without it the run stops on the loop all the same, naming the term it came back to instead of running the budget down. Under morph nothing is asked for: 𝕄 always has a term to answer with, a loop 𝔻 meets under a firing parks the site the firing stands at, and the walk of --deep goes on to the next binding.

What a frame remembers is the branch from the run down to it, never everything the run has touched, so two sibling subterms that happen to be written alike stay two terms and only a term genuinely reached from itself is a loop. The cut costs one lookup and fires on the turn the repeat appears, so raising --max-steps from 40 to a million changes neither the answer nor the time. The flag promises nothing about programs that loop without ever repeating a term — a body that grows on every round rather than coming back still ends on the budget.

Rewrite

You can rewrite this expression with the help of rules defined in the my-rule.yml YAML file (here, the !d is a capturing group, similar to regular expressions):

name: My custom rule
pattern: Δ ⤍ !d
result: Δ ⤍ 62-79-65

Then, rewrite:

$ phino rewrite --rule=my-rule.yml hello.phi
⟦ φ ↦ ⟦ Δ ⤍ 62-79-65 ⟧, t ↦ ξ.k, k ↦ ⟦⟧ ⟧

If you want to use many rules, just use --rule as many times as you need:

phino rewrite --rule=rule1.yaml --rule=rule2.yaml ...

You can also use built-in rules, which are designed to normalize expressions:

phino rewrite --normalize hello.phi

Both flags may be combined, so that your own rules are applied alongside the built-in ones, in a single rewriting session:

phino rewrite --normalize --rule=my-rule.yaml hello.phi

Some rules mint fresh synthetic names via the random-string built-in. To keep the output reproducible across runs, phino seeds the random generator deterministically with 0 by default. Use --seed to pick a different seed:

phino rewrite --seed=42 --rule=my-rule.yml hello.phi

If no input file is provided, the 𝜑-expression is taken from stdin:

$ echo '⟦ φ ↦ ⟦ Δ ⤍ 68-65-6C-6C-6F ⟧ ⟧' | phino rewrite --rule=my-rule.yml
⟦ φ ↦ ⟦ Δ ⤍ 62-79-65 ⟧ ⟧

You're able to pass XMIR as input. Use --input=xmir and phino will parse given XMIR from file or stdin and convert it to phi AST.

phino rewrite --rule=my-rule.yaml --input=xmir file.xmir

Also phino supports 𝜑-expressions in ASCII format and with syntax sugar. The rewrite command also allows you to desugar the expression and print it in canonical syntax:

$ echo '[[ @ -> Q.io.stdout("hello") ]]' | phino rewrite
⟦
  φ ↦ Φ.io.stdout(
    α0 ↦ Φ.string( φ ↦ Φ.bytes( φ ↦ ⟦ Δ ⤍ 68-65-6C-6C-6F, ρ ↦ ∅ ⟧ ) )
  ),
  ρ ↦ ∅
⟧

Merge

You can merge several 𝜑-expressions into a single one by merging their top level formations:

$ cat bytes.phi
⟦ bytes ↦ ⟦ φ ↦ ∅ ⟧ ⟧
$ cat number.phi
⟦
  number ↦ ⟦
    φ ↦ ∅,
    plus(x) ↦ ⟦ λ ⤍ L_number_plus ⟧
  ⟧
⟧
$ cat minus.phi
⟦ number ↦ ⟦ minus(x) ↦ ⟦ λ ⤍ L_number_minus ⟧ ⟧ ⟧
$ phino merge bytes.phi number.phi minus.phi --sweet
⟦
  bytes(φ) ↦ ⟦⟧,
  number(φ) ↦ ⟦
    plus(x) ↦ ⟦ λ ⤍ L_number_plus ⟧,
    minus(x) ↦ ⟦ λ ⤍ L_number_minus ⟧
  ⟧
⟧

Match

You can test the 𝜑-expression matches against the rule pattern. The result output contains matched substitutions:

$ phino match --pattern='⟦ Δ ⤍ !d, !B ⟧' hello.phi
B >> ⟦ ρ ↦ ∅ ⟧
d >> 68-65-6C-6C-6F

Explain

You can explain the built-in rules by printing them in LaTeX format. Pass exactly one of --normalize, --morph, --dataize or --contextualize for the rewriting, morphing (𝕄), dataization (𝔻) or contextualization (𝒞) rules (or --rule for a custom rule file):

$ phino explain --normalize
\begin{tabular}{rl}
\phinoNormalizationRule{alpha}
  { [[ B_1, \tau -> ?, B_2 ]] ( \phiTerminal{\alpha_{i}} -> e ) }
  { [[ B_1, \tau -> ?, B_2 ]] ( \tau -> e ) }
  { $ i = \vert \overline{ B_1 } \vert $ }
  { }
\phinoNormalizationRule{dc}
  { T ( \tau -> e ) }
  { T }
  { }
  { }
...
\phinoNormalizationRule{stop}
  { [[ B ]] . \tau }
  { T }
  { $ \tau \notin B \;\text{and}\; @ \notin B \;\text{and}\; L \notin B $ }
  { }
\end{tabular}

The morphing and dataization rules are printed the same way:

$ phino explain --morph
\begin{tabular}{rl}
\phinoMorphingRule{mf}
  { \mathbb{M}( [[ B ]], e ) }
  { [[ B ]] }
  { }
  { }
...
\phinoMorphingRule{universe}
  { \mathbb{M}( Q, e ) }
  { \mathbb{M}( \phinoNormalize{ e }, e ) }
  { $ e \not= Q $ }
  { }
\end{tabular}

$ phino explain --dataize
\begin{tabular}{rl}
\phinoDataizationRule{delta}
  { \phinoDataize{ [[ B_1, D> \delta_0, B_2 ]] } }
  { \delta_0 }
  { }
  { }
...
\phinoDataizationRule{norm}
  { \phinoDataize{ n } }
  { \phinoDataize{ \mathbb{M}( n, e ) } }
  { }
  { }
\end{tabular}

$ phino explain --contextualize
\begin{phinoContextualizationInference}
  \phinoName{cxi}
  \phinoConclusion{ \phinoContextualize{ \phiTerminal{\xi} }{ k }{ k } }
\end{phinoContextualizationInference}
...
\begin{phinoContextualizationInference}
  \phinoName{cd}
  \phinoPremise{ \phinoContextualize{ n }{ k }{ n_1 } }
  \phinoConclusion{ \phinoContextualize{ n . \tau }{ k }{ n_1 . \tau } }
\end{phinoContextualizationInference}

For more details, use phino [COMMAND] --help option.

Rule structure

This is BNF-like yaml rule structure. Here types ended with apostrophe, like Attribute' are built types from 𝜑-expression AST

Rule:
  name: String
  pattern: String
  result: String
  when: Condition?       # predicate, works with substitutions before extension
  where: [Extension]?    # substitution extensions
  having: Condition?     # predicate, works with substitutions after extension

Condition:
  = and: [Condition]     # logical AND
  | or:  [Condition]     # logical OR
  | not: Condition       # logical NOT
  | eq:                  # compare two comparable objects
      - Comparable
      - Comparable
  | in:                  # check if attributes exist in bindings
      - Attribute'
      - Binding'
  | nf: Expression'      # returns True if given expression in normal form
                         # which means that no more other normalization rules
                         # can be applied
  | absolute: Expression' # returns True if given expression is xi-free, i.e.
                         # there is no ξ outside of a formation: it is Φ, a
                         # formation, a dispatch with a xi-free subject, or an
                         # application with a xi-free subject and argument.
                         # Combined with a normal-form check by the '𝑘'/'!k'
                         # meta variable, which ranges over the absolute
                         # expressions 𝒦 ⊆ 𝒩, used by the Rcopy rule.
  | matches:             # returns True if given expression after dataization
      - String           # matches to given regex
      - Expression
  | part-of:             # returns True if given expression is attached to any
      - Expression'      # attribute in ginve bindings
      - BiMeta'
  | formation:           # returns True if given expression is a formation
      Expression'        # (an abstraction ⟦…⟧); used by morphing 'md'
                         # as 'not (formation 𝑛)', so a non-formation head is
                         # morphed and a formation head is left to 'ml'
  | gt:                  # returns True if the first comparable object is
      - Comparable       # greater than the second one
      - Comparable
  | disjoint:            # returns True if none of the given attributes exists
      - [Attribute']     # in the given bindings
      - Binding'

Comparable:              # comparable object that may be used in 'eq' condition
  = Attribute'
  | Number
  | Expression'

Number:                  # comparable number
  = Integer              # just regular integer
  | IndexMeta'           # 𝑖 (or !i), the index captured by an α𝑖 argument
  | length: BiMeta'      # calculate length of bindings by given meta binding
  | domain: BiMeta'      # calculate number of unique attributes in given
                         # meta binding (excluding 'assets')

Extension:               # substitutions extension used to introduce new meta variables
  meta: [ExtArgument]    # new introduced meta variable
  function: String       # name of the function
  args: [ExtArgument]    # arguments of the function

ExtArgument
  = Bytes'               # !d
  | Binding'             # !B
  | Expression'          # !e
  | Attribute'           # !t

Here's list of functions that are supported for extensions:

• contextualize - function of two arguments, that rewrites given expression depending on provided context according to the contextualization rules
• random-tau - creates an attribute with a random unique name. It accepts no arguments; uniqueness is guaranteed across all names already taken in the document.
• dataize - dataizes given expression and returns bytes.
• concat - accepts bytes or dataizable expressions as arguments, concatenates them into single sequence and convert it to expression that can be pretty printed as human readable string: Φ.string(Φ.bytes⟦ Δ ⤍ !d ⟧).
• sed - pattern replacer, works like unix sed function. Accepts two arguments: target expression and pattern. Pattern must start with s/, consists of three parts separated by /, for example, this pattern s/\\s+//g replaces all the spaces with empty string. To escape braces and slashes in pattern and replacement parts - use them with \\, e.g. s/\\(.+\\)//g.
• random-string - accepts dataizable expression or bytes as pattern. Replaces %x and %d formatters with random hex numbers and decimals accordingly. Uniqueness is guaranteed during one execution of phino.
• size - accepts exactly one meta binding and returns size of it and Φ.number.
• tau - accepts Φ.string, dataizes it and converts it to attribute. If dataized string can't be converted to attribute - an error is thrown.
• string - accepts Φ.string or Φ.number or attribute and converts it to Φ.string.
• number - accepts Φ.string and converts it Φ.number
• sum - accepts list of Φ.number or Φ.bytes and returns sum of them as Φ.number
• join - accepts list of bindings and returns list of joined bindings. Duplicated ρ, Δ and λ attributes are ignored, all other duplicated attributes are replaced with unique attributes using random-tau function.

Meta variables

The phino supports meta variables to write 𝜑-expression patterns for capturing attributes, bindings, etc.

This is the list of supported meta variables:

• !t || 𝜏 - attribute
• !i || 𝑖 - the index of a positional (α) application argument, captured by writing α𝑖 (or ~!i)
• !e || 𝑒 - any expression
• !n || 𝑛 - any expression that is already in normal form (behaves like !e/𝑒, but only binds a sub-expression in NF, so no explicit nf: guard is needed)
• !k || 𝑘 - any expression that is absolute, i.e. xi-free and in normal form (ranges over 𝒦 ⊆ 𝒩); behaves like !e/𝑒 but only binds an absolute sub-expression, so no explicit absolute: or nf: guard is needed
• !B || 𝐵 - list of bindings
• !d || 𝛿 - bytes in meta delta binding
• !F || 𝑓 - function name in meta lambda binding
• !S || 𝜎 - a symbol standing where a λ name stands (see Symbols). It is spelled the way a meta variable is spelled but is a name and no capture: 𝜎1 is one concrete symbol, which no substitution ever binds, and a bare 𝜎 in the answer of a --symbolic entry asks for a fresh one

A meta variable carries a suffix, like !B1 or 𝜏2, to name what it captured, so that the result, when, where and having of a rule can read it back. An index starts with one: a suffix of 0, as in !B0 or 𝜏0, is refused where it is written, because it is a first index spelled wrong and no name. A positional argument keeps counting from zero, though, since α0 is an index of the calculus and no meta variable.

Written bare, with no suffix at all, a meta variable is anonymous: it matches whatever term stands in its place, every occurrence on its own, and binds no name. Two anonymous metas of one kind are therefore two different captures, which is what lets a pattern ask for any two attributes without inventing names for them:

name: two-attributes
pattern: '⟦ 𝜏 ↦ 𝑒, 𝜏 ↦ 𝑒 ⟧'
result: '⟦ x ↦ ⟦ Δ ⤍ 2A- ⟧ ⟧'

Spelled with suffixes, that pattern would read ⟦ 𝜏1 ↦ 𝑒1, 𝜏2 ↦ 𝑒2 ⟧ and name four captures the result never mentions, while ⟦ 𝜏1 ↦ 𝑒1, 𝜏1 ↦ 𝑒1 ⟧ would be rejected as a duplicated attribute.

Nothing can refer to an anonymous meta, since it has no name to be referred to by. Writing one outside a pattern (or the match, e-match and c-match of an inference rule) is a mistake in the rule and is reported as the rule loads.

A positional (α) application argument is written as α0, ~0 (ASCII), or α𝑖/~!i when its index is captured by an !i/𝑖 meta variable.

Incorrect usage of meta variables in 𝜑-expression patterns leads to parsing errors.

Benchmark

To run performance benchmarks, you need Java 8+ and curl. Maven is downloaded automatically on first run via benchmark/mvnw.

The benchmark uses the compiled Native class from JNA — a large real-world Java class — as its test input. On first run, make bench downloads the class, disassembles it to XMIR via jeo-maven-plugin, converts it to 𝜑 using phino rewrite, and caches the results in benchmark/tmp/. Subsequent runs skip straight to the benchmarks.

Besides parsing, printing and rewriting that class, the suite morphs symbolically. benchmark/demo.phi is a small world whose entries name the λ functions of benchmark/atoms.yaml, and each entry is a case of its own, so that a slowdown of one of them is a line of the report rather than a share of a single total. The smallest entry — one λ function fired against one unknown — is timed twice, over the demo world alone and over the same world merged into the class, and the two numbers say between them what the world around an entry costs (see #1291).

A case whose single run is measured in seconds gets fewer warmups and fewer batches than a case measured in microseconds, since the whole suite runs inside one job; the report says how many of each a case was given.

make bench

=== parse/phi ===
  warmup:     3 iterations
  batches:    10 x 1
  total:      1821425.151 μs
  avg:        182142.515 μs
  min:        170750.493 μs
  max:        209499.629 μs
  std dev:    15132.778 μs
=== parse/xmir ===
  warmup:     3 iterations
  batches:    10 x 1
  total:      7708084.189 μs
  avg:        770808.419 μs
  min:        701670.454 μs
  max:        827995.748 μs
  std dev:    39123.293 μs
=== rewrite/normalize ===
  warmup:     3 iterations
  batches:    10 x 1
  total:      507305.249 μs
  avg:        50730.525 μs
  min:        48912.624 μs
  max:        54335.144 μs
  std dev:    1596.161 μs
=== print/sweet/multiline ===
  warmup:     3 iterations
  batches:    10 x 1
  total:      4188218.626 μs
  avg:        418821.863 μs
  min:        403263.572 μs
  max:        449353.774 μs
  std dev:    14512.853 μs
=== print/sweet/flat ===
  warmup:     3 iterations
  batches:    10 x 1
  total:      4025720.702 μs
  avg:        402572.070 μs
  min:        382540.835 μs
  max:        428138.472 μs
  std dev:    11933.717 μs
=== print/salty/multiline ===
  warmup:     3 iterations
  batches:    10 x 1
  total:      14045902.469 μs
  avg:        1404590.247 μs
  min:        1384313.216 μs
  max:        1438197.181 μs
  std dev:    15501.328 μs
=== morph/symbolic/demo/e1 ===
  warmup:     3 iterations
  batches:    10 x 1
  total:      880309.436 μs
  avg:        88030.944 μs
  min:        86359.252 μs
  max:        90267.072 μs
  std dev:    1248.861 μs
=== morph/symbolic/demo/e2 ===
  warmup:     3 iterations
  batches:    10 x 1
  total:      1215850.964 μs
  avg:        121585.096 μs
  min:        117038.580 μs
  max:        138033.783 μs
  std dev:    5877.028 μs
=== morph/symbolic/demo/e3 ===
  warmup:     3 iterations
  batches:    10 x 1
  total:      1844780.073 μs
  avg:        184478.007 μs
  min:        180633.446 μs
  max:        192191.924 μs
  std dev:    3471.827 μs
=== morph/symbolic/demo/e4 ===
  warmup:     3 iterations
  batches:    10 x 1
  total:      617914.516 μs
  avg:        61791.452 μs
  min:        60976.930 μs
  max:        62245.020 μs
  std dev:    354.771 μs
=== morph/symbolic/demo/e5 ===
  warmup:     3 iterations
  batches:    10 x 1
  total:      185308.236 μs
  avg:        18530.824 μs
  min:        17898.792 μs
  max:        19243.924 μs
  std dev:    442.924 μs
=== morph/symbolic/native/e5 ===
  warmup:     2 iterations
  batches:    4 x 1
  total:      18057164.992 μs
  avg:        4514291.248 μs
  min:        4280917.084 μs
  max:        4860213.506 μs
  std dev:    215452.202 μs

The results were calculated in this GHA job on 2026-09-20 at 06:19, on Linux with 4 CPUs.

How to Contribute

Fork repository, make changes, then send us a pull request. We will review your changes and apply them to the master branch shortly, provided they don't violate our quality standards. To avoid frustration, before sending us your pull request please make sure all your tests pass:

make all

To generate a local coverage report for development, run:

make coverage

To build a phino executable into the root of the repository, run:

make phino

This produces an executable phino (or phino.exe on Windows) in the project root, which you can run directly for quick local testing:

./phino --version

You will need GHC ≥ 9.6.7 and Cabal ≥ 3.0 (recommended) or Stack ≥ 3.0 installed.