ISAR.TensorSemantics

Term model: tensors are ITerms; extensional equality is IRed-joinability (confluence is IRed_confluence). Combinators B/C/W are SKI encodings so dup/swap/comp β-laws are theorems, not axioms.

source

@[reducible, inline]

abbrev ISAR.TensorSpace :

Type

Equations

ISAR.TensorSpace = ISAR.ITerm

Instances For

source

def ISAR.ExtEq (t u : TensorSpace) :

Prop

Equations

ISAR.ExtEq t u = ∃ (v : ISAR.ITerm ), ISAR.IRed t v ∧ ISAR.IRed u v

Instances For

source

theorem ISAR.ExtEq.refl (t : TensorSpace) :

ExtEq t t

source

theorem ISAR.ExtEq.symm {t u : TensorSpace} :

ExtEq t u → ExtEq u t

source

theorem ISAR.ExtEq.trans {t u w : TensorSpace} (h1 : ExtEq t u) (h2 : ExtEq u w) :

ExtEq t w

source

def ISAR.t_norm :

TensorSpace

Equations

ISAR.t_norm = ISAR.ITerm.norm

Instances For

source

def ISAR.t_konst :

TensorSpace

Equations

ISAR.t_konst = ISAR.ITerm.konst

Instances For

source

def ISAR.t_var :

Nat → TensorSpace

Equations

ISAR.t_var = ISAR.ITerm.var

Instances For

source

def ISAR.t_app :

TensorSpace → TensorSpace → TensorSpace

Equations

ISAR.t_app = ISAR.ITerm.app

Instances For

source

def ISAR.t_comp :

TensorSpace

B = S (K S) K.

Equations

ISAR.t_comp = ISAR.t_app (ISAR.t_app ISAR.ITerm.sₛ (ISAR.t_app ISAR.ITerm.konst ISAR.ITerm.sₛ)) ISAR.ITerm.konst

Instances For

source

def ISAR.t_dup :

TensorSpace

W = S S (K I).

Equations

ISAR.t_dup = ISAR.t_app (ISAR.t_app ISAR.ITerm.sₛ ISAR.ITerm.sₛ) (ISAR.t_app ISAR.ITerm.konst ISAR.ITerm.norm)

Instances For

source

def ISAR.t_swap :

TensorSpace

C = S (S (K B) S) (K K).

Equations

One or more equations did not get rendered due to their size.

Instances For

source

theorem ISAR.t_app_congr {t1 t2 u1 u2 : TensorSpace} (ht : ExtEq t1 t2) (hu : ExtEq u1 u2) :

ExtEq (t_app t1 u1) (t_app t2 u2)

source

theorem ISAR.t_app_congr_left {t1 t2 u : TensorSpace} (h : ExtEq t1 t2) :

ExtEq (t_app t1 u) (t_app t2 u)

source

theorem ISAR.t_app_congr_right {t u1 u2 : TensorSpace} (h : ExtEq u1 u2) :

ExtEq (t_app t u1) (t_app t u2)

source

theorem ISAR.t_norm_beta (x : TensorSpace) :

ExtEq (t_app t_norm x) x

source

theorem ISAR.t_konst_beta (x y : TensorSpace) :

ExtEq (t_app (t_app t_konst x) y) x

source

theorem ISAR.t_comp_app_f (f : TensorSpace) :

IRed (t_app t_comp f) (t_app ITerm.sₛ (t_app ITerm.konst f))

source

theorem ISAR.t_comp_red (f g x : TensorSpace) :

IRed (t_app (t_app (t_app t_comp f) g) x) (t_app f (t_app g x))

source

theorem ISAR.t_comp_beta (f g x : TensorSpace) :

ExtEq (t_app (t_app (t_app t_comp f) g) x) (t_app f (t_app g x))

source

theorem ISAR.t_dup_red (f x : TensorSpace) :

IRed (t_app (t_app t_dup f) x) (t_app (t_app f x) x)

source

theorem ISAR.t_dup_beta (f x : TensorSpace) :

ExtEq (t_app (t_app t_dup f) x) (t_app (t_app f x) x)

source

theorem ISAR.t_swap_red (f x y : TensorSpace) :

IRed (t_app (t_app (t_app t_swap f) x) y) (t_app (t_app f y) x)

source

theorem ISAR.t_swap_beta (f x y : TensorSpace) :

ExtEq (t_app (t_app (t_app t_swap f) x) y) (t_app (t_app f y) x)

source

def ISAR.t_sₛ :

TensorSpace

Equations

One or more equations did not get rendered due to their size.

Instances For

source

theorem ISAR.t_s_beta (x y z : TensorSpace) :

ExtEq (t_app (t_app (t_app t_sₛ x) y) z) (t_app (t_app x z) (t_app y z))

source

def ISAR.denot :

ITerm → TensorSpace

Equations

Instances For

source

theorem ISAR.denot_sound {t u : ITerm} (h : IStep t u) :

ExtEq (denot t) (denot u)

source

theorem ISAR.denot_sound_red {t u : ITerm} (h : IRed t u) :

ExtEq (denot t) (denot u)

source

@[implicit_reducible]

instance ISAR.tensorSetoid :

Setoid TensorSpace

Equations

ISAR.tensorSetoid = { r := ISAR.ExtEq, iseqv := ISAR.tensorSetoid._proof_1 }

source

def ISAR.ExtTensor :

Type

Equations

ISAR.ExtTensor = Quotient ISAR.tensorSetoid

Instances For

source

noncomputable def ISAR.denot_ext (t : ITerm) :

ExtTensor

Equations

ISAR.denot_ext t = Quotient.mk ISAR.tensorSetoid (ISAR.denot t)

Instances For

source

theorem ISAR.denot_factors (t u : ISKSubtype) (h : OperEq t u) :

denot_ext t.val = denot_ext u.val

source

noncomputable def ISAR.InvariantLayer.toExtTensor :

InvariantLayer → ExtTensor

The final semantic map from Invariant Layer quotient classes into extensional tensors.

Equations

ISAR.InvariantLayer.toExtTensor = Quotient.lift (fun (t : ISAR.ISKSubtype) => ISAR.denot_ext t.val) ⋯

Instances For

source

inductive ISAR.LEq :

LTerm → LTerm → Prop

Operational equivalence on lambda terms, defined as the equivalence relation generated by LStep.

of_step {t u : LTerm} : LStep t u → LEq t u
refl (t : LTerm) : LEq t t
symm {t u : LTerm} : LEq t u → LEq u t
trans {t u w : LTerm} : LEq t u → LEq u w → LEq t w

Instances For

source

@[implicit_reducible]

instance ISAR.lambdaSetoid :

Setoid LTerm

Equations

ISAR.lambdaSetoid = { r := ISAR.LEq, iseqv := ISAR.lambdaSetoid._proof_1 }

source

def ISAR.LambdaQuotient :

Type

The operational quotient of lambda terms.

Equations

ISAR.LambdaQuotient = Quotient ISAR.lambdaSetoid

Instances For

source

noncomputable def ISAR.lambda_denot_ext (t : LTerm) :

ExtTensor

Equations

ISAR.lambda_denot_ext t = Quotient.mk ISAR.tensorSetoid (ISAR.denot (ISAR.compile t))

Instances For

source

theorem ISAR.lambda_denot_sound (t u : LTerm) (h : LEq t u) :

ExtEq (denot (compile t)) (denot (compile u))

source

theorem ISAR.lambda_denot_factors (t u : LTerm) (h : LEq t u) :

lambda_denot_ext t = lambda_denot_ext u

source

noncomputable def ISAR.LambdaQuotient.toExtTensor :

LambdaQuotient → ExtTensor

The semantic map from the operational quotient of lambda terms into extensional tensors.

Equations

ISAR.LambdaQuotient.toExtTensor = Quotient.lift (fun (t : ISAR.LTerm) => ISAR.lambda_denot_ext t) ⋯

Instances For

source

def ISAR.lapp_raw (t u : LTerm) :

LTerm

Equations

ISAR.lapp_raw t u = t.app u

Instances For

source

theorem ISAR.lapp_congruence_left (t1 t2 u : LTerm) (h : LEq t1 t2) :

LEq (t1.app u) (t2.app u)

source

theorem ISAR.lapp_congruence_right (t u1 u2 : LTerm) (h : LEq u1 u2) :

LEq (t.app u1) (t.app u2)

source

theorem ISAR.lapp_congruence (t1 t2 u1 u2 : LTerm) (ht : LEq t1 t2) (hu : LEq u1 u2) :

LEq (lapp_raw t1 u1) (lapp_raw t2 u2)

source

def ISAR.LambdaQuotient.app (t u : LambdaQuotient) :

LambdaQuotient

Application of quotient classes in LambdaQuotient.

Equations

t.app u = Quotient.lift₂ (fun (t u : ISAR.LTerm) => Quotient.mk ISAR.lambdaSetoid (ISAR.lapp_raw t u)) ISAR.LambdaQuotient.app._proof_1 t u

Instances For

source

noncomputable def ISAR.t_app_ext (t u : ExtTensor) :

ExtTensor

Lifted application in ExtTensor.

Equations

ISAR.t_app_ext t u = Quotient.lift₂ (fun (t u : ISAR.TensorSpace) => Quotient.mk ISAR.tensorSetoid (ISAR.t_app t u)) ISAR.t_app_ext._proof_1 t u

Instances For

source

theorem ISAR.toExtTensor_app (t u : LambdaQuotient) :

(t.app u).toExtTensor = t_app_ext t.toExtTensor u.toExtTensor

Compilation is a homomorphism for application up to tensor extensional equivalence.

source

def ISAR.obs_a :

TensorSpace

Equations

ISAR.obs_a = ISAR.t_norm

Instances For

source

def ISAR.obs_b :

TensorSpace

Equations

ISAR.obs_b = ISAR.t_konst

Instances For

source

theorem ISAR.NormalI.norm :

NormalI ITerm.norm

source

theorem ISAR.NormalI.konst :

NormalI ITerm.konst

source

theorem ISAR.NormalI.konst_konst :

NormalI (ITerm.konst · ITerm.konst)

source

theorem ISAR.non_trivial_observable :

¬ExtEq (t_app obs_a obs_b) obs_a

source

theorem ISAR.non_trivial_observable2 :

¬ExtEq (t_app (t_app obs_a obs_b) obs_b) obs_a

source

theorem ISAR.separation_lemma {A B : TensorSpace} (x y : TensorSpace) (h_neq : ¬ExtEq (t_app (t_app A x) y) (t_app (t_app B x) y)) :

¬ExtEq A B

source

noncomputable def ISAR.t_K :

TensorSpace

Equations

ISAR.t_K = ISAR.t_app (ISAR.t_app ISAR.t_comp ISAR.t_konst) ISAR.t_norm

Instances For

source

noncomputable def ISAR.t_K2 :

TensorSpace

Equations

ISAR.t_K2 = ISAR.t_app (ISAR.t_app ISAR.t_comp ISAR.t_konst) (ISAR.t_app (ISAR.t_app ISAR.t_comp ISAR.t_konst) ISAR.t_norm)

Instances For

source

theorem ISAR.t_K_beta (x y : TensorSpace) :

ExtEq (t_app (t_app t_K x) y) x

source

theorem ISAR.t_K2_beta (x y z : TensorSpace) :

ExtEq (t_app (t_app (t_app t_K2 x) y) z) x

source

theorem ISAR.adequacy_norm_konst (M N : LTerm) (hM : LRed M (LTerm.var 0).abs) (hN : LRed N (LTerm.var 1).abs.abs) :

¬ExtEq (denot (compile M)) (denot (compile N))

source

theorem ISAR.adequacy_konst_k2 (M N : LTerm) (hM : LRed M (LTerm.var 1).abs.abs) (hN : LRed N (LTerm.var 2).abs.abs.abs) :

¬ExtEq (denot (compile M)) (denot (compile N))

source

theorem ISAR.adequacy_norm_k2 (M N : LTerm) (hM : LRed M (LTerm.var 0).abs) (hN : LRed N (LTerm.var 2).abs.abs.abs) :

¬ExtEq (denot (compile M)) (denot (compile N))

source

inductive ISAR.Fam3 :

Type

I : Fam3
K : Fam3
K2 : Fam3

Instances For

source

def ISAR.Fam3.toLTerm :

Fam3 → LTerm

Equations

ISAR.Fam3.I.toLTerm = (ISAR.LTerm.var 0).abs
ISAR.Fam3.K.toLTerm = (ISAR.LTerm.var 1).abs.abs
ISAR.Fam3.K2.toLTerm = (ISAR.LTerm.var 2).abs.abs.abs

Instances For

source

theorem ISAR.adequacy_family (a b : Fam3) (h : a ≠ b) :

¬ExtEq (denot (compile a.toLTerm)) (denot (compile b.toLTerm))