목록에 '고유'를위한 더 빠른 코드

Question

이 질문은 Isabelle/HOL 정리 정리기를 사용한 코드 생성을 참조합니다.

나는 목록

export_code distinct in Scala file - 

나는 다음과 같은 코드

def member[A : HOL.equal](x0: List[A], y: A): Boolean = (x0, y) match { 
    case (Nil, y) => false 
    case (x :: xs, y) => HOL.eq[A](x, y) || member[A](xs, y) 
} 

def distinct[A : HOL.equal](x0: List[A]): Boolean = x0 match { 
    case Nil => true 
    case x :: xs => ! (member[A](xs, x)) && distinct[A](xs) 
} 

이 코드는 차 런타임이에게 얻을

에 distinct 기능에 대한 코드를 내보낼 때. 더 빠른 버전이 있습니까? 내 이론의 시작 부분에 문자열에 대해 "~~/src/HOL/Library/Code_Char"을 가져 오는 것과 같은 것을 생각하고 효율적인 코드 생성을 설정합니다. distinct의 더 나은 구현은 O (n log n)에서 목록을 정렬하고 목록을 한 번 반복하는 것입니다. 그러나 나는 더 잘할 수 있다고 생각 하나?

어쨌든 distinct의 구현이 더 빠르며 Main의 다른 기능을 사용할 수 있습니까?

Answer 1

나는 Isabelle2013의 라이브러리에 더 빨리 구현의 모르겠지만, 다음과 같이 당신은 스스로를 쉽게 수행 할 수 있습니다

1. 은 정렬 된 목록에 구별 성을 결정하는 기능 distinct_sorted를 구현합니다.
2. 는 distinct_sorted 참으로 정렬 된 목록에 distinct
3. 이 distinct_list 및 정렬을 통해 distinct를 구현하는 보조 정리를 증명하고 distinct에 대한 새로운 코드 식으로 선언 구현하고 있음을 증명한다. 다음과 같이

은 요약하면,이 보인다 :

context linorder begin 
fun distinct_sorted :: "'a list => bool" where 
    "distinct_sorted [] = True" 
| "distinct_sorted [x] = True" 
| "distinct_sorted (x#y#xs) = (x ~= y & distinct_sorted (y#xs))" 

lemma distinct_sorted: "sorted xs ==> distinct_sorted xs = distinct xs" 
    by(induct xs rule: distinct_sorted.induct)(auto simp add: sorted_Cons) 
end 

lemma distinct_sort [code]: "distinct xs = distinct_sorted (sort xs)" 
by(simp add: distinct_sorted) 

다음, 당신은 효율적인 정렬 알고리즘이 필요합니다. 기본적으로 sort은 삽입 정렬을 사용합니다. HOL/Library에서 Multiset을 가져 오면 sort이 quicksort에 의해 구현됩니다. 형식 증명의 아카이브에서 Efficient Mergesort을 가져 오면 병합 정렬이됩니다.

효율성을 향상시킬 수는 있지만 방해가됩니다. 위의 선언 후에 요소가 linorder 클래스의 인스턴스 인 목록에서만 distinct을 실행할 수 있습니다. 이 상세 검색은 코드 생성기 내에서만 발생하므로 Isabelle의 정의와 정리는 영향을받지 않습니다. HOL/Library에서 List_lexord가 사전 식 순서를 선택하여 그렇게, 그러나 이것은에 선형 순서가 필요합니다 코드 식의 목록의 목록에 distinct을 적용하는 예를 들어

은, 먼저 목록에 선형 순서를 정의해야 집단. char list을 약어로 사용하는 string을 사용하려는 경우 Char_ord은 에 대한 일반적인 순서를 정의합니다. 문자를 Code_Char으로 대상 언어의 문자 유형으로 매핑하는 경우 Char_ord을 사용하는 경우 적응 이론 Code_Char_ord도 필요합니다.