Fall '05 SIGALG and SIGTHEORY will meet jointly.
This seminar does not meet every week. Each talk is announced by
email. Contact saunders@udel.edu to be added
to the announcements list.
Seminars are held at 4:00pm Wednesdays in 102a Smith Hall, unless they're not.
All sessions are open to any interested person.
Title: Introspective hybrid algorithms for integer matrix linear algebra (continued)
Title: Introspective hybrid algorithms for integer matrix linear algebra
Speaker: David Saunders, CIS Dept, UDel.
Abstract:
I will discuss hybrids for rank, determinant, system solution, and
Smith Normal Form. Several methods will be illustrated to combine high
performance on typical cases encountered in practice with a guarantee
of performance within a constant factor of optimal on worst case inputs.
I will also report on some related developments discussed last week at the
Banff International Research Station workshop "Challenges in Linear and
Polynomial Algebra in Symbolic Computation Software".
Title: Machine Self-Reference Applied to Sentences
Speaker: John Case, CIS Dept, UDel.
Abstract:
Goedel's proof of his famous First Incompleteness Theorem featured, in
the context of languages of arithmetic, what we will call propositional
self-reference. He created a sentence which asserted the unprovability of a
(trivially) provably equivalent sentence. Feferman subsequently published a
lemma providing more general propositional self-reference.
Kleene's Strong Recursion Theorem, which has many applications in computability theory, provides analogous self-reference, but for algorithms instead of sentences. The $n$-ary version of Kleene's Theorem, stemming from Smullyan's 2-ary version, has been applied occasionally. The speaker's infinitary version has had many applications.
In this talk we show how to prove a strong, infinitary variant of Feferman's Lemma from Kleene's Theorem and we provide some new applications to the theory of arithmetic. For example, we give a direct proof of a theorem of Myhill's on the existence of absolutely independent sentences of arithmetic. We use this correct proof and a failed, even more direct variant to discuss that: sometimes one can prove a theorem by writing down what one wants in terms of self-referential sentences and, then, one has it (with very little additional argument); but other times the connection between the self-referential sentences employed and what's to be proved is less clear. We point too to other applications of infinitary self-reference, for example, an analog in arithmetic of the Busy~Beaver Function's being unbounded by a computable function.
We also indicate how our proofs provide the insight that proving metatheorems about arithmetic is much more like programming in a subrecursive programming system than it is like programming in, say, an acceptable programming system (for the entire class of partial computable functions). For example, Tarski's Theorem (first known to Goedel) that arithmetic cannot express its own truth-definition is seen to be perfectly analogous to the result that a subrecursive system does not contain a universal program for that system.