[prev in list] [next in list] [prev in thread] [next in thread] 

List:       lyx-devel
Subject:    Re: Official submission of eLyXer for inclusion in LyX
From:       rgheck <rgheck () bobjweil ! com>
Date:       2009-04-29 22:09:43
Message-ID: 49F8D027.2040308 () bobjweil ! com
[Download RAW message or body]

Alex Fernandez wrote:
> Hi Richard,
> 
> On Wed, Apr 29, 2009 at 4:31 PM, rgheck <rgheck@bobjweil.com> wrote:
> 
> > So far as I can see, math is almost untranslated at this point. (I just
> > cloned from git.) Theorem-type environments do not get converted, either.
> > There's more on this in a different message.
> > 
> 
> That is not really true. All formulae in the LyX User Guide are
> translated correctly and without errors. The only errors are related
> to custom macros and some weird bracketing when using \displaystyle
> and friends (the whole formula is surrounded by {}). The LyX Math
> Guide outputs a lot of errors, but the big majority are a question of
> adding a translation to a config file.
> 
> 
The document I converted ended up with very little but raw LaTeX. I 
don't know why, but that's how it went. E.g.:

   1. N0
   2. N/x/\/wedge//Pxy/→N/y/
   3. \/forall//x/\/forall//y/\/forall//z/(N/x/\/wedge//Pxy/\/wedge//Pxz/→/y/ = /z/)

   4. \/forall//x/\/forall//y/\/forall//z/(N/x/\/wedge/N/y/\/wedge//Pxz/\/wedge//Pyz/→/x/ = /y/)

   5. \/neg/\/exists//x/(N/x/\/wedge//Px/0)
   6. \/forall//x/(N/x/→\/exists//y/(/Pxy/))
   7. \/forall//F/(/F/0\/wedge/\/forall//x/\/forall//y/(N/x/\/wedge//Fx/\/wedge//Pxy/→/Fy/)→\/forall//x/(N/x/→/Fx/)



Pretty ugly. I'll put another paragraph at the end. Some of it is custom 
macros, but anyone who uses much math at all will have custom macros.

> > I don't want to be a party-pooper, but under these circumstances I can't
> > agree that eLyXer is "ready for prime time".
> > 
> 
> It is for many people who just need basic math (like me and, I would
> contend, 90% of LyX users). 
> 
> 
It would surprise me if 90% of LyX users only needed "basic math".

> The rest will have to add a bit of work,
> if only to report errors or send sample documents. Saying "math is
> almost untranslated" is not helpful.
> 
> 
Well, sorry, but I wasn't trying to be helpful. I was speaking to Pavel, 
and he was asking how the math rendering was. So I told him that, in my 
testing, math is almost untranslated, which it is.

Let me say again that my point had to do with what's required if this is 
to be included in LyX. And my view, which I would expect to be widely 
shared, is that support for "basic math" isn't good enough *for that 
purpose*. If it works well enough for you and some other users, that's 
great, and I have no problem with supporting it the same way we support 
htlatex, i.e., by detecting it and configuring an exporter, etc.

Just to be clear, here are what I regard as the showstoppers: 
Theorem-type environments aren't rendered; math support is marginal, esp 
with regard to custom macros; BibTeX isn't supported, so far as I can 
tell; cross-references omit the related text. Other things I'd want to 
investigate would include support for AMS environments, and arrays and 
the like generally; treatment of mini pages and the like. I also worry 
about the lack of extensibility, i.e., the inability to deal with custom 
styles.

Of course, it's up to you, and other people who want to work on eLyXer 
whether to address these issues, or instead to ignore them and say, 
"This is good enough for us". It's up to us to decide how it relates to LyX.

Richard


=====

Another math example. Some of these are just unsupported standard 
macros; others are custom macros of mine. Surely this is enough to 
justify the "almost untranslated" remark.

Finally, \/Pi/_1 ^1 comprehension is needed for the proof of axiom (7), 
that is, for the proof of mathematical induction. The point is easy to 
overlook. I have often said in lectures on Frege, and may even have said 
in print, that Frege defines the natural numbers as "the numbers for 
which induction works". But that is not quite right, as a close look at 
how Frege actually defines the natural numbers reveals. Frege defines 
the ‘strong' ancestral of a relation /R/ as follows:
\/sanc//Rab/\/eqdf/\/forall//F/[\/forall//x/(/Rax/→/Fx/)\/wedge/\/forall//x/\/forall//y/(/Fx/\/wedge//Rxy/→/Fy/)→/Fb/],  \


and the ‘weak' ancestral as:
\/wanc//Rab/\/eqdf/\/sanc//Rab/\/vee//a/ = /b/.
It is then easy to prove, /via/ predicative comprehension, that:
\/wanc//Rab/\/equiv/\/forall//F/[/Fa/\/wedge/\/forall//x/\/forall//y/(/Fx/\/wedge//Rxy/→/Fy/)→/Fb/]. 

Frege then defines the concept of natural number as:
\/BigN//n/\/eqdf/\/wanc//P/0/n/, 
where the relation /P/ is that of predecession, defined in a way we 
shall see shortly. We then have immediately that
\/BigN//n/→\/forall//F/[/F/0\/wedge/\/forall//x/\/forall//y/(/Fx/\/wedge//Pxy/→/Fy/)→/Fn/],  

which is equivalent to:
\/forall//F/[/F/0\/wedge/\/forall//x/\/forall//y/(/Fx/\/wedge//Pxy/→/Fy/)→\/forall//x/(\/BigN//x/→/Fx/)]. \


But this is weaker than (7), due to the absence of \/BigN//x/ from the 
antecedent of /Fx/\/wedge//Pxy/→/Fy/. Now if we instantiate /F/ with 
\/BigN/\/xi/\/wedge//Fx/, thus arriving at:
\/forall//F/\{(\/BigN/0\/wedge//F/0)\/wedge/\/forall//x/\/forall//y/[(\/BigN//x/\/wedge//Fx/)\/wedge//Pxy/ \
→(\/BigN//y/\/wedge//Fy/)]→\/forall//x/[\/BigN//x/→(\/BigN//x/\/wedge//Fx/)]\ 

then (7) will follow quickly, but this move depends upon comprehension, 
specifically upon the availability of
\/exists//G/\/forall//x/[/Gx/\/equiv/\/BigN//x/\/wedge//Fx/], 
and the definition of \/BigN/ contains bound second-order quantifiers: 
It is, more precisely, \/Pi/_1 ^1 . So \/Pi/_1 ^1 comprehension is 
sufficient here, but it also seems to be necessary.


[prev in list] [next in list] [prev in thread] [next in thread]