Nuprl Definition : very-dep-fun

We want to descibe a process "f,g" where "f" assignin to b ∈ B
a term a ∈ A  and "g" computes a value r ∈ C[a;b] to get a triple
<a, b, r> ∈ a:A × b:B × C[a;b].
Given a list bs ∈ B List, this process "f,g" thus accumulates a list of
triples L ∈ (a:A × b:B × C[a;b]) List, but on each new b ∈ bs, f can use
the list L accumuated so far -- i.e. if b = bs[i], f can uses the list
accumulated by "f,g" from firstn(i;bs).

The type of "g" is simply a:A ⟶ b:B ⟶ C[a;b].
The type of "f" could simply be ((a:A × b:B × C[a;b]) List) ⟶ B ⟶ A
but that would require ⌜f L b ∈ A⌝ for any list of triples L, and b ∈ B.

Instead, we only need ⌜f L b ∈ A⌝  for lists L where if
  <a, b, r> = L[i] then   a = (f firstn(i;L) b).

We write ⌜vdf-eq(A;f;L)⌝ for this constraint on L.
Then the type of f should be
f ∈ {L:(a:A × b:B × C[a;b]) List| vdf-eq(A;f;L)}  ⟶ B ⟶ A

So the type of the domain of f mentions f itself.
This is what we call a very dependent function type.

To define this type we use the dependent intersection type.
We define, by induction on n, the type vdf(A;B;a,b.C[a; b];n) of very dependent
functions that can accept input lists L of length upto n.
Then the very dependent function type is the intersection of these.
very-dep-fun(A;B;a,b.C[a; b]) ==  ⋂n:ℤ. vdf(A;B;a,b.C[a; b];n)

The constraint vdf-eq(A;f;L) is also defined by induction on the length of L
using dependent intersection.

By induction on n we can prove vdf-wf+ which proves (jointly) that
vdf-eq(A;f;L) is a proposition and vdf(A;B;a,b.C[a;b];n) is a type,
and also that vdf-eq(A;f;L) ⊆r (∀[i:ℕ||L||]. ((fst(L[i])) = (f firstn(i;L) (fst(snd(L[i])))))).

We get a kind of elimination rule for very-dep-fun(A;B;a,b.C[a; b])
Error :very-dep-fun-subtype  that says that for
f ∈ very-dep-fun(A;B;a,b.C[a; b])  we have
f ∈ {L:(a:A × b:B × C[a;b]) List| vdf-eq(A;f;L)}  ⟶ B ⟶ A

For an introduction rule, we have a tactic VeryDepFunCD that reduces
proving f ∈ very-dep-fun(A;B;a,b.C[a;b])  to proving that
f [] ∈ B ⟶ A   and  f L ∈ B ⟶ A under the assumption
∀[i:ℕ||L||]. ((fst(L[i])) = (f firstn(i;L) (fst(snd(L[i])))))

To use the elimination rule, we will need to verify that a list of triples
L satisfies ⌜vdf-eq(A;f;L)⌝. For that, we have a tactic ProveVdfEq
that reduces that to proving
(fst(L[j])) = (f firstn(j;L) (fst(snd(L[j]))))
under the assumption
∀[i:ℕj]. ((fst(L[i])) = (f firstn(i;L) (fst(snd(L[i])))))

So the upshot is that we should be able to treat the type
very-dep-fun(A;B;a,b.C[a; b]) as an abstract, primitive type using only
the lemma Error :very-dep-fun-subtype and the tactics
VeryDepFunCD and ProveVdfEq.

⋅

very-dep-fun(A;B;a,b.C[a; b]) == ⋂n:ℤ. vdf(A;B;a,b.C[a; b];n)

Definitions occuring in Statement : vdf: vdf(A;B;a,b.C[a; b];n), isect: ⋂x:A. B[x], int: ℤ
Definitions occuring in definition : isect: ⋂x:A. B[x], int: ℤ, vdf: vdf(A;B;a,b.C[a; b];n)
FDL editor aliases : very-dep-fun

Latex:
very-dep-fun(A;B;a,b.C[a; b]) == \mcap{}n:\mBbbZ{}. vdf(A;B;a,b.C[a; b];n) Date html generated: 2020_05_19-PM-09_40_19 Last ObjectModification: 2020_03_09-AM-11_31_41 Theory : co-recursion-2 Home Index