Re: Lean4 and dependent type theory

--000000000000e05b2605d241f7cd
Content-Type: text/plain; charset="UTF-8"

> Are you aware of any LEAN4 design documents that addresses these
questions?

No. The best reference for Lean's type system is Theorem Proving in Lean; a
version has been ported to Lean 4.

Jeremy

On Fri, Dec 3, 2021 at 12:04 PM Tim Daly <[email protected]> wrote:

> Axiom allows the user to dynamically create dependent types.
> For example, matrix(3,3) is a 3x3 matrix. This may
> seem trivial but it is not.
>
> Consider that to construct the "domain" (as it is called
> in Axiom) of 3x3 matrices you need to evaluate the
> arguments. Again, in this case it is trivial but, in general,
> it is not. Among other things it defines what functions
> are available to manipulate 3x3 matrices, e.g. inverse.
>
> Several issues arise. One is the "representation" (aka
> "carriers" in logic-speak). There is no reason to assume
> that the entries are integers. In the new Axiom (aka SANE)
> the "representation" is orthogonal to the domain and can
> be specified at construction.
>
> Axiom allows matrices that contain anything. When
> constructing a new matrix, e.g. [[2.3,...],[4.4,...]..] the
> entries may be from other "domains", in this case the
> floats. But they could just as well be polynomials. So
> from matrix(3,3) you need to dynamically construct
> matrix(3,3,FLOAT).
>
> Another issue is inheriting theorems and definitions that
> support the newly constructed domain. In the new Axiom,
> the theorems and definitions are associated with the
> "category hierarchy". They are inherited based on the
> dynamically constructed domain. These are available to
> prove functions in the constructed domain.
>
> A matrix(3,3) is commutative but matrix(3,4) is not. The
> property of commutativity is inherited from the hierarchy
> but only for square matrices. This has to be decided at
> the time the domain is constructed.
>
> This allows proofs of functions in the 3x3 domain to use
> the commutative theorems of square matrices. These
> are not available for functions in the 3x4 domain.
> So, clearly, we need to evaluate the arguments when
> constructing the domain.
>
> Ah, but evaluating the arguments of a dependent type is
> NOT trivial in general. You could, for example, construct
> domains which contain themselves in the argument,
> such as matrix(matrix(...
>
> More fun exists because one could, for example, introduce
> a new "category" into the hierarchy that has additional
> definitions and theorems related to square matrices over
> some new domain. These have to be dynamically inherited
> in particular cases.
>
> Worse yet, the elements don't have to be PROP but
> could be anywhere in the type hierarchy. The elements
> could be functors, for example.
>
> I've spent a great deal of time pondering these problems.
>
> My current "solution path" involves constructing objects
> in CLOS (Common Lisp Object System) which allows me
> to achieve very fine-grained control due to the MOP
> (Meta Object Protocol). In addition, I'm trying to make the
> domains as "declarative" as possible so that most of the
> details are not hidden in obscure code.
>
> CLOS allows both dynamic construction and dynamic
> re-shaping. I have no idea how LEAN4 will handle these
> without the MOP.
>
> Are you aware of any LEAN4 design documents that addresses
> these questions?
>
>

--000000000000e05b2605d241f7cd
Content-Type: text/html; charset="UTF-8"
Content-Transfer-Encoding: quoted-printable

<div dir=3D"ltr">&gt; Are you aware of any LEAN4 design documents that addr=
esses these questions?<div><br></div><div>No. The best reference for Lean&#=
39;s type system is Theorem Proving in Lean; a version has been ported to L=
ean 4.</div><div><br></div><div>Jeremy</div></div><br><div class=3D"gmail_q=
uote"><div dir=3D"ltr" class=3D"gmail_attr">On Fri, Dec 3, 2021 at 12:04 PM=
 Tim Daly &lt;<a href=3D"mailto:[email protected]">[email protected]</a>&=
gt; wrote:<br></div><blockquote class=3D"gmail_quote" style=3D"margin:0px 0=
px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div =
dir=3D"ltr"><div>Axiom allows the user to dynamically create dependent type=
s.</div><div>For example, matrix(3,3) is a 3x3 matrix. This may</div><div>s=
eem trivial but it is not.</div><div><br></div><div>Consider that to constr=
uct the &quot;domain&quot; (as it is called</div><div>in Axiom) of 3x3 matr=
ices you need to evaluate the</div><div>arguments. Again, in this case it i=
s trivial but, in general,</div><div>it is not. Among other things it defin=
es what functions</div><div>are available to manipulate 3x3 matrices, e.g. =
inverse.<br></div><div><br></div><div>Several issues arise. One is the &quo=
t;representation&quot; (aka</div><div>&quot;carriers&quot; in logic-speak).=
 There is no reason to assume <br></div><div>that the entries are integers.=
 In the new Axiom (aka SANE)</div><div>the &quot;representation&quot; is or=
thogonal to the domain and can</div><div>be specified at construction.<br><=
/div><div><br></div><div>Axiom allows matrices that contain anything. When<=
/div><div>constructing a new matrix, e.g. [[2.3,...],[4.4,...]..] the</div>=
<div>entries may be from other &quot;domains&quot;, in this case the</div><=
div>floats. But they could just as well be polynomials. So</div><div>from m=
atrix(3,3) you need to dynamically construct</div><div>matrix(3,3,FLOAT).<b=
r></div><div><br></div><div>Another issue is inheriting theorems and defini=
tions that</div><div>support the newly constructed domain. In the new Axiom=
,</div><div>the theorems and definitions are associated with the</div><div>=
&quot;category hierarchy&quot;. They are inherited based on the <br></div><=
div>dynamically constructed domain. These are available to</div><div>prove =
functions in the constructed domain.<br></div><div><br></div><div>A matrix(=
3,3) is commutative but matrix(3,4) is not. The</div><div>property of commu=
tativity is inherited from the hierarchy</div><div>but only for square matr=
ices. This has to be decided at</div><div>the time the domain is constructe=
d.<br></div><div><br></div><div>This allows proofs of functions in the 3x3 =
domain to use</div><div>the commutative theorems of square matrices. These<=
/div><div>are not available for functions in the 3x4 domain.<br></div><div>=
So, clearly, we need to evaluate the arguments when</div><div>constructing =
the domain.</div><div><br></div><div>Ah, but evaluating the arguments of a =
dependent type is</div><div>NOT trivial in general. You could, for example,=
 construct</div><div>domains which contain themselves in the argument,</div=
><div>such as matrix(matrix(... <br></div><div><br></div><div>More fun exis=
ts because one could, for example, introduce</div><div>a new &quot;category=
&quot; into the hierarchy that has additional</div><div>definitions and the=
orems related to square matrices over</div><div>some new domain. These have=
 to be dynamically inherited</div><div>in particular cases.<br></div><div><=
br></div><div>Worse yet, the elements don&#39;t have to be PROP but <br></d=
iv><div>could be anywhere in the type hierarchy. The elements</div><div>cou=
ld be functors, for example.<br></div><div><br></div><div>I&#39;ve spent a =
great deal of time pondering these problems.</div><div><br></div><div>My cu=
rrent &quot;solution path&quot; involves constructing objects</div><div>in =
CLOS (Common Lisp Object System) which allows me</div><div>to achieve very =
fine-grained control due to the MOP</div><div>(Meta Object Protocol). In ad=
dition, I&#39;m trying to make the</div><div>domains as &quot;declarative&q=
uot; as possible so that most of the</div><div>details are not hidden in ob=
scure code. <br></div><div><br></div><div>CLOS allows both dynamic construc=
tion and dynamic <br></div><div>re-shaping. I have no idea how LEAN4 will h=
andle these <br></div><div>without the MOP.<br></div><div><br></div><div>Ar=
e you aware of any LEAN4 design documents that addresses</div><div>these qu=
estions?<br></div><div><br></div></div>
</blockquote></div>

--000000000000e05b2605d241f7cd--