Vega 데이터 변환을 위한 형식 의미론(Formal Semantics) 및 타입 시스템(Type System)

Vega는 대화형 데이터 시각화(interactive data visualizations)를 생성하기 위한 인기 있는 선언적 언어(declarative language)입니다. Vega는 스트리밍 데이터플로우 아키텍처(streaming dataflow architecture)를 사용하여 반응형 데이터 변환(reactive data transformations)을 지원합니다. 널리 채택되었음에도 불구하고, Vega의 정확한 의미론(semantics)은 미묘하며 문서화가 제대로 되어 있지 않습니다. 이는 부정확하거나 혼란스러운 시각화 및 이해하기 어려운 에러 메시지로 이어집니다. 본 논문은 두 가지 기여를 합니다. 첫째, 그래프 기반의 운영 의미론(graph-based operational semantics)을 정의하여 Vega의 스트리밍 데이터플로우 아키텍처에 대한 정밀한 모델을 제공합니다. 둘째, 다양한 일반적인 오류를 방지할 수 있는 Vega의 핵심 데이터 변환 언어를 위한 타입 시스템(type system)을 제시합니다. 우리는 우리의 타입 시스템이 의미론에 대해 건전함(sound)을 보여줍니다. Vega의 데이터플로우 아키텍처는 함수형 반응형 프로그래밍(functional reactive programming) 및 적응형 계산(adaptive computation)과 같이 잘 연구된 모델들과 밀접하게 닮아 있지만, 중요한 차이점들이 존재합니다. 우리 연구의 독창성은 이러한 차이점들을 정밀하게 규명하고, 이러한 반응형 데이터 시각화 언어에 대한 정적 분석(static analysis)을 제공한다는 점에 있습니다. 그 결과, 실제 환경에서 발생하는 일반적인 오류를 잡아낼 수 있는 Vega용 체커(checker)를 구현하였습니다.