Extracting computational content from classical proofs (5月14日,Mizuhito Ogawa )

Mizuhito Ogawa (小川 瑞史,School of Information Science, Japan Advanced Institute of Science and Technology)
星期三, 五月 14, 2014 - 15:00 to 16:00

内容简介:Abstract: Program extraction from a constructive proof has been investigated from 1980's. Recently, there are several trials to extract from classical proofs. The difficulties maiinly lie in excluded middle and axiom of choice, and the former are investigated by Minlog groups. This talk discusses on the latter, the case study on finite basis properties based on Higman's lemma. For Higman's lemma, by converting the standard proof by minimal bad sequences to open induction, we obtain a constructive proof. However, a classically equivalent finite basis property has more quantifier alternations, and the same technique does not work. We pose a question why a case study (in "A linear time algorithm for monadic querying of indefinite data over linearly ordered domains. Inf. Comput. 186(2), 2003") on the finite basis property still works.\r\n