Name has something to do with proof theory
Has a good proof theory
linear + non-linear (with overloading. same function can be used in linear or non-linear way)
type?? inference
overloading
Types
Simplest type: empty type or unit
DBT: 'I hate the empty type'. Why?
Types with one element
----- ---------
(): 1 (): value
Type with
So the important this is the +.
ie, the 'Either' type. Left or right. Ability to distinguish between the two directions. => sum type
Type:
e: A e: B
------------- -------------
inl e: A + B inr e: A + B
Value:
v: value v value
------------- -------------
inl v: value inr v: value
Example:
- true = inl ()
- false = inr ()
Working with binary sum is cumbersome. So multi-way sum??
+{e: Aₑ | e ← L} such that L≠∅ and L is finite
L is an index set.
A+B = +{inl: A, inr: B} bool = +{true: 1, false: 1}
The : 1 is a tag.
Can L be recursive? Yes.
Example: nat
nat = +{zero: 1, succ: nat}
[0] = zero ()
[1] = succ (zero ())
[2] = succ (succ (zero ()))
DBT: This is equirecursive types. Not just isomorphic types.
Note: sum cannot have recursion. This has.
Typing rules for +.
k (v) means k tagging a value
(k ∈ L) e: Aₖ
----------------------- +i
k (e): +{l: Aₗ | l ∈ L}
DBT: What is A ?
Try a list of nats:
list = +{nil: 1, cons: nat * list }
Now we need pair type.
e1: A e2: B v1: val v2: val
------------------- ----------------------
(e1, e2): A*B (v1, v2): val
We got few rules to construct elements. Now we need rules to actually compute with them.
Try negation of bools.
A function like: nat (x: bool): bool
Got to do case (ie, patmat).
nat x =
match x with
| true u => false u
| false u => true u
end
true and false are tags. u here will be unit/1.
This is fine too:
nat x =
match x with
| true u => false ()
| false u => true ()
end
But in linear programming (aka garbage free programming), every var would be used exactly once. No garbage => no need of garbage collection. And in the above snippet, u is not used. So better not go with that.
Now we got patmat. Got to give rules to type that.
Δ ⊢ e: +{
----------------------------------
Δ,Γ ⊢ match e with (l(x) -> eₗ) l∈L : C
dup x = (x, x) not valid in LFP
Disjoint union
Γ is either empty or one var with another Γ ??
Γ := ()
| Γ, x:A
Δ ⊢ e1: A Γ ⊢ e2: B
------------------------
Δ,Γ ⊢ (e1, e2): A*B
Empty context can prove only one thing.
------------
x: A ⊢ x: A
k x y = x not valid ∵ y not used.
Δ ⊢ e: A*B Γ x:A y:B ⊢ e':C
-------------------------------------
match e with (x,y) => e': C
An example.
plus (x: nat) (y: nat): nat
plus x y =
match x with
| zero () => y
| succ x' => succ (plus x' y)
end
Or
plus x y =
match x with
| zero () => y
| succ x' => plus x' (succ y)
end
Second one is tail recursive!
DBT: (match on x or y doesn't matter. It's a symmetric function ???)
Linear program: use up all its vars, but only once.
plus (x: nat) (y: nat): nat
plus x y =
match x with
| zero u => y
| succ x' => succ (plus x' y)
end
This is wrong, I guess? Because u is not used.
—
Tags and labels.
Variable name clashes: Got to be different.
Product of n elements: Has to be lazy
Pair has no labels
Γ ⊢ e: Aₖ (k ∈ L)
----------------------- +i
Γ ⊢ k (e): +{l: Aₗ | l ∈ L}
—
type bool = +{'true:1, 'false: 1}
decl not (x: bool): bool
defn not x = match x with
| 'true() => 'false()
| 'false() => 'true()
; $ ./snax --out=none hi.adj0
; % loading file hi.adj0
; % default mode: L
; %%----- values
; %%-----
; % success
decl false: bool
defn false = not ('true ())
type nat = +{'zero:1, 'succ: nat}
decl three: nat
defn three = succ (succ (succ (zero())))
type list = +{'nil: 1, 'cons: nat * list}
Reversing a list: It should be linear.
HW: mult, exp
drop and copy for nat mult => inefficiency ??
You probably shouldn't be using this kind of copy/drop
drop, copy any given type
Benefits of linear proging: no need of GC
The reverse can be made to be in-place. Space reuse. Conversion to C. Not all programs/function addition should be linear. If it isn't, it's probably a bug
No higher order functions in SNAX. map isn't there ?
At least not in adj0 (level 0)
------------
x: A ⊢ x: A
------------
⋅ ⊢ (): 1
Δ⊢e1: A Γ⊢e2: B
--------------------------
Δ,Γ⊢(e1, e2): A*B
Δ⊢e: 1 Γ⊢e': C
-------------------------------
Δ,Γ⊢(match e with () => e'): C
Δ⊢e: A*B Γ,x:A,y:B⊢e': C
-------------------------------
Δ,Γ⊢(match e with (x,y) => e'): C
sum intro
Γ⊢e: Aₖ | k∈L
-------------------------
Γ ⊢ k(e): +{l:Aₗ | l ∈ L}
sum destr
Δ⊢e:+{l:Aₗ | l∈L} Aₖ | k∈L
-------------------------
Γ ⊢ k(e): +{l:Aₗ | l ∈ L}
Setting up the logic system is the real deal. Proof is routine.
Closer the correspondance between dynamcis and statiscs => easeir ther proofs ???
Let η is env (ie, a variable map) for context Γ. While writing inference rules, write what you know first and follow from there.
Already passed type checker => single use guaraneetted ???
Subtractive approach. Spit out unused context. It has some problems.
Additive approach. Spit out used context.
—
In addtivie approach, if Γ ⊢ e:A \ Ω then
If Ω ⊢ e:A and Ω⊆Γ, then
η1⊢e1-->v1\ω1 η2⊢e2-->v2\ω2
-----------------------------------
η1,η2⊢(e1,e2) --> (v1,v2) \ (ω1,ω2)
—
Γ⊢e:A \ Ω η:Γ ω:Ω v:A
-----------------------------
η ⊢ e-->v\ω
adding lambdas. complicated, but still like done so far. merge operation affine logic: vars can be used at most once. are the evaluation rules and typing rules isomorphic? No, some discrepancies.
------------
⋅ A ⊢ A
Original natural deduction
Linear logic:
- * is circled: tensor
Top definitions. Fully linear language => can't accomplish much ??
Linear logic
A,B := 1 | A*B | A+B
| !A (of course A. Allows assumption re-use. Use ordinary logic within linear??)
| A lollipop B (like implication. Notin Snax yet ??)
| A&B (conjunction)
Positive can be duplicated, but not negative ?? So negative need !.`
A => B is !A lollipop B
1+1 ⊢ (1+1) * (1+1)
Copy of boolean type
Extracting proof from program ???? As long as logic is constructive ??
A -> B -> A cannot be proved??? Because B is never used.
Γ,A ⊢ B
Γ⊢A->B
Γ⊢λx:A.e: A-> B
Γ⊢A->B Δ⊢A
Γ,Δ ⊢ B
can't patmat on lambdas. Can apply it though. Indicative of difference between positive and negative types. Observing structres?? Negaive => can't observe structure, but can use them. & is lazy ??
& lazy record, or external choice
positive => can look at their structure. we can observe them dirly => can duplicate them negative => apply / project component. can't just drop/duplicate
recursive lazy record => OOP
map fn is not linear. because f has to be applied in n times
For now (adj1), !A is any top-level defns. ∵ they can be used as many times as needed.
type nat = +{'zero: 1, 'succ: nat}
type list = +{'nil: 1, 'cons: nat*list}
decl map (f: nat -> nat) (xs: list): list
defn map f xs =
match xs with
| 'nil() => 'nil()
| 'cons(x,xs) => 'cons(f x, map f xs)
(*
% loading file one.adj1
% default mode: L
one.adj1:8.26-8.39:error:
variable f of mode L used more than once
| 'cons(x,xs) => 'cons(f x, map f xs)
~~~~~~~~~~~~~
% static checking failed
*)
Problems:
It reports the first one it come across (here, it uses the additive approach)
Modes:
U
/ \
A S
\ /
L
$ snax -m A file.ajd1
A:
% loading file one.adj1 % default mode: A one.adj1:8.26-8.39:error: variable f of mode A used more than once
| 'cons(x,xs) => 'cons(f x, map f xs) |
~~~~~~~~~~~ % static checking failed
S:
% loading file one.adj1 % default mode: S one.adj1:7.5-7.11:error: variable f of mode S not used in all branches
| 'nil() => 'nil() |
~~~~ % static checking failed
shell returned 1
We should be able to write fns like map. Soln could be to be able to mix linear and non-linear modes.
Replacing map by an iterator??
A,Bₘ ::= 1 | A*B | +{l:Aˡₘ | l∈L} | ↓ᵏₘAₖ (where k≥m)
| A -o B | &{l:Aˡₘ | l∈L} | ↑ᵏᵢAₖ (where k≤i)
shift operators to switch between modes ??
—
U list but L elements. Nah.. ∵ throw away list => throw away elems, which are linear
L list but U elements ??
—
=Δ
mode polymorphism mode inference
lazy, eager
—
Independence in typing rules:
Γ ⊢ e: Aₘ
Γ ≥ m
—
Syntax:
fΓ≥k Γ ⊢ e: Aₖ
------------------
Γ ⊢ <e>: ↓ᵏₘ
where k≥m
and Γ≥m ????
Paper: https://arxiv.org/abs/2402.01428
Ability to controlling memory layout
Semi-Axiomatic Sequent Calculus
LNL (Linear and non-linear logic combined) 1995 Benton
Contraction: Can dup a val Weakening: Can drop
Γ,A,A ⊢ C ———– contraction Γ,A⊢C
Proof theory: Read Bottom up Prog: Top down
Γ⊢A ———– dup Γ,C ⊢ A
Positive type => can observe it. ie, can patmat.
Neg type
sequent calculus considering a higher-level, non-flat memory layout
-------------
A,B⊢A*circleB
---
⋅⊢1
semi axiomatci ∵ half the rules in Gentzen's version is replaced by axioms ??
Cut-rule
Futures in FP. can execute in llel, but need to wait if commn is needed ??
cut is like allocation
Dynamics:
SSOS: Sub Structural Operational Semantics
cells and processes
Sequential => processes are gone over left to right llel => any ordering
In this semantics, we write to empty cells. But we can mutate ??
proc(cut x P(x); Q(x)) -> proc(P(a)), proc(Q(a)) where a is a newly allocated cell.
cell a □, proc(write a V) -> cell a V
# move b to a
cell a □, cell b V, proc(id a b) -> cell a V
Γ
Memory data layout
https://arxiv.org/abs/2212.06321v3
Δ⊢A Γ,A̲⊢C
------------- snip (positive)
Δ,Γ⊢C
where A is a sub-formula of C.
Then it's not a cut, but what Frank calls a 'snip'.
Δ⊢A̲ Γ,A⊢C
------------- snip (negative)
Δ,Γ⊢C
Γ (context, statics): vars ↦ typesη: Γ (environment, dynamis): vars ↦ values(let ((default-directory "/tmp"))
(shell-command "ls"))
(buffer-file-name)