학교강의필기장/프로그래밍언어론

Syntactic Sugar구문 설탕은 언어의 표현력을 증가시키진 않지만 프로그램을 더 읽고 쓰기 편하게 만들어준다. 예를 들어, let x = E1 in E2도 사실 설탕에 속하는데, 여기서 설탕을 빼면 (proc x E2) E1이 된다.let x = 1 in let y = 2 in x + y위와 같은 구문이, => (proc (x) (let y = 2 in x + y)) 1=> (proc (x) ((proc (y) (x + y)) 2)) 1설탕이 빠지면 이렇게 난잡해진다. 즉 우리가 사용한 기존 문법에서,let x = E1 in E2 ⇒ (proc (x) E2) E1 로 설탕을 쳐낼 수 있고letrec f(x) = E1 in E2 ⇒ let f = proc (x) (E1) in E2 으로 설탕..

Let-Polymorphic Type Checking Algorithmlet 다형성을 지원하는 타입 체크 알고리즘은 재계산을 피하고 효율적으로 타입 체크를 수행하기 위해 더 정교한 알고리즘을 사용한다. 1. Γ라는 타입 환경에서 표현식 e1을 찾기 위해 일반적인 타입 체크 알고리즘을 사용한다. (U(V(Γ, e1, t)))2. 타입 일반화: 타입 t에서 남아있는 변수를 일반화해서 type scheme, ∀α1 ... α_n.t 을 구한다. 이들은 t에서 나타나는 타입 변수들이다.3. 바인드된 변수 x에 대해 타입 스킴을 기록하도록 타입 환경을 확장하고, e2에 대해 타입 체크를 시작한다.4. x의 각 발생마다 새로운 타입 변수 β1 ... β_n을 생성하고 이를 사용하여 타입 스킴을 인스턴스화 한다. 위..

자동 타입 추론 문제자동 타입 추론은 주어진 프로그램 E에 대해 가장 일반적인 타입을 추론하는 문제이다. E가 타입을 가질 수 있는 경우 이를 결정하는 타입을 찾아내고, 그렇지 않은 경우에는 타입을 가질 수 없음을 표시한다. 자동 타입 추론은 정적 분석(static analysis) 알고리즘으로, 표현식의 사용 방식을 관찰하여 타입을 추론한다. 이 알고리즘은 정확(sound)하고 완전(complete)하다. 즉, 분석이 표현식에 대해 타입을 찾는다면 그 표현식은 잘 타입된 것이고, 표현식이 타입 시스템에 따라 타입을 가지면 분석은 그 타입을 반드시 찾아낸다. 이 알고리즘은 아래 두 단계로 구성된다. 1. 프로그램 텍스트에서 타입 방정식 생성2. 방정식 풀이 타입 방정식은 각 서브 표현식과 변수에 대해 타..

Motivation현재까지, 문법과 의미를 엄밀하게 정의하고 정식 설계를 반영한 인터프리터를 구현함으로써 Program → Interpreter → Result 구조의 언어를 설계하였다.그러나 현재 시스템에는 안전하지 않은 프로그램을 실행하려 시도하여 런타임 에러가 발생할 수 있다. (C++, Python, JS 등의 언어가 그렇다) 따라서 프로그램의 안전성을 분석하고 모든 버그를 정적으로 탐지하는 자동화된 기술을 만들어야 한다.Program → Analyzer → Interpreter → Result Static Analyzer는 정적, 그리고 자동으로 소프트웨어 버그를 감지한다.static: 실행 전에 프로그램 텍스트를 분석한다.automatic: Static Analyzer로 sw를 분석한다. 이는..

레코드Records란 이름이 있는 메모리의 모음이다. 즉, C언어의 struct와 유사하다. 물론 배열 또한 메모리 위치들의 모음이지만 이 위치들의 이름은 자연수, index이다. SyntaxE → ...       | {}       | { x:= E, y := E }       | E.x       | E.x := E ValuesVal = Z + Bool + {.} + Procedure + Record + Loc Procedure = Var × E × Envr ∈Record = Field → Locp ∈ Env = Var → Locσ ∈ Mem = Loc → Val Semantics빈 레코드의 결과는 . 이고, 메모리는 바뀌지 않는다. x := E1, y := E2로 초기화 되는 레코드를 생성한다.환..

Syntax & SemanticsSyntax : 메모리 위치 생성 및 사용 (변수 선언, 할당 참조 등)신텍스는 프로그래밍 언어에서 메모리 위치 생성 및 사용하는 방법을 정의한다. 이를 통해 변수나 데이터 구조를 저장하고 조작할 수 있다. Semantics: 메모리 상태 조작 (특정 변수에 값 할당 시, 메모리 위치에 새로운 값 저장)시맨틱스는 프로그램이 실행될 때 메모리의 상태가 어떻게 변하는지를 정의한다. 변수에 값을 할당하거나 변수 값을 변경하는 작업을 포함한다. 언어의 상태를 추가함으로써 메모리의 상태를 동적으로 변화시킬 수 있고, 단순한 값 계산 외로도 다양한 부수 효과를 처리할 수 있다. let counter = 0in let f = proc (x) (let counter = counter +..

Procedures를 추가해보자 P → E // 프로그램은 표현식으로 구성된다. E → n // 표현식은 다음 중 하나일 수 있다. | x // 변수 생성 가능 | E + E // 덧셈 가능 | E - E // 뺄셈 가능 | (E) // 괄호 가능 | iszero E // 간단한 함수 (0인지 확인) | if E then E else E // 조건문 가능 | let x = E in E // 지역 변수에 표현식 할당 | read // 입력 5강에서, 우리는 위 Syntax를 만들었었다. 우리는 이제 여기에 아래 두 개를 추가할 것이다. | proc x E | E E proc x E는 인자 x를 받아 E를 실행하는 함수를 정의한다. E E는 함수를 호출하는데 사용될 것이다. Free/Bound Variabl..

Syntax & Semantics 프로그래밍 언어를 설계할 때 가장 중요한 두 가지 요소는 문법(Syntax)과 의미(Semantics)이다. Syntax는 프로그램을 어떻게 작성해야 하는지에 대한 규칙을 정의한다. 프로그램의 구조를 결정하고, 변수, 키워드, 연산자, 구문 등 언어의 요소들이 어떻게 조합되어야 하는지를 명시한다. Semantics는 프로그램이 실제로 어떤 동작을 수행하는지에ㅍ 대한 정의이다. Syntax와 Semantics는 귀납적 정의(Inductive Definitions)로 명시될 수 있다. 첫 번째 언어 구축 먼저, Let이라는 이름의 간단한 언어를 만들어보자. Syntax P → E // 프로그램은 표현식으로 구성된다. E → n // 표현식은 다음 중 하나일 수 있다. | x..