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
活动地址: 
锡昌堂(哲学系)322

内容简介: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