Autocomplete

위키 검색창의 자동완성 모듈. 사용자가 타이핑하는 동안 실시간으로 후보를 제시하므로, 정확한 제목을 기억하지 못해도 원하는 문서에 빠르게 도달할 수 있다.

매칭 우선순위는 사용자의 검색 의도를 반영한다: 정확 일치 > 시작 일치 > 끝 일치 > 포함 순으로 우선순위가 정해지며, 이는 "Java"를 검색할 때 "Java"가 "JavaScript"보다 먼저 나와야 하는 직관과 일치한다.

검색 결과는 pagename 기준으로 중복 제거된다. 같은 pagename에 여러 alias가 매칭되면, 최고 점수(가장 낮은 score 값)만 유지된다. 이 불변량이 깨지면 같은 페이지가 결과에 여러 번 나타난다.

module dedup

sig Pagename {}

sig SearchEntry {
  pagename: one Pagename,
  score: one Int
}

sig DedupResult {
  entries: set SearchEntry
}

-- 결과에 같은 pagename의 엔트리가 둘 이상 없음
fact noDuplicatePagename {
  all r: DedupResult | all disj e1, e2: r.entries |
    e1.pagename != e2.pagename
}

-- 결과에 포함된 엔트리는 해당 pagename의 최소 점수를 가짐
fact bestScoreKept {
  all r: DedupResult, e: r.entries |
    no other: SearchEntry |
      other.pagename = e.pagename and other.score < e.score
}

-- 모든 pagename은 결과에 대표가 있음
fact allPagenamesCovered {
  all r: DedupResult |
    all p: SearchEntry.pagename |
      some e: r.entries | e.pagename = p
}

-- 위 fact들이 동시에 만족 가능한지 확인 (vacuous satisfaction 방지)
assert nonVacuous {
  some r: DedupResult | some r.entries
}

-- 최고 점수 엔트리가 반드시 선택됨
assert bestAlwaysWins {
  all r: DedupResult, e: r.entries |
    all other: SearchEntry |
      other.pagename = e.pagename implies e.score <= other.score
}

check bestAlwaysWins for 5 but 6 Int

run nonVacuousCheck { some r: DedupResult | #r.entries > 1 } for 5 but 6 Int

alloy:model(dedup)

검색 매칭

searchEntries는 쿼리와 인덱스를 비교하여 점수순으로 정렬된 결과를 반환한다. 공백은 무시하고 매칭하므로 "helloworld"로 "Hello World"를 찾을 수 있다.

import { searchEntries } from './src/lib/autocomplete-search.ts'
const r = searchEntries([
  ['JavaScript', 'JavaScript'],
  ['Java', 'Java'],
  ['TypeScript', 'TypeScript'],
], 'java')
console.log(JSON.stringify({ first: r[0][0], second: r[1][0] }))

searchResult={"first":"Java","second":"JavaScript"}

run:wiki

expr	expected
.first	Java
.second	JavaScript

하이라이트

검색 결과에서 매칭된 부분을 시각적으로 강조한다. 사용자가 자신의 쿼리가 어떻게 매칭되었는지 즉시 확인할 수 있어, 여러 후보 중 원하는 문서를 빠르게 식별하는 데 도움이 된다.

한국어의 경우 초성 검색을 지원하므로 "ㄱㄴ"을 입력하면 "가나다라"에서 "가나"가 하이라이트된다. 이는 한국어 사용자가 자음만으로 빠르게 검색하는 습관을 반영한 설계다.

text	query	expected
Hello World	hel	<mark>Hel</mark>lo World

text	chosungQuery	expected
가나다라	ㄱㄴ	<mark>가나</mark>다라