Синтаксические категории Exp4

Сентябрь 7, 2022

Главная
Алгебра
Синтаксические категории Exp4

Содержание

2. Отношение ⇒ языка Exp4 Оно имеет две составляющие: арифметическую ρ├ e =>А v и булеву ρ├
3. Естественная семантика языка Exp4 Правило CR Правило VarR Правило OpR Правило LocR ρ├ n ⇒A n
4. Естественная семантика языка Exp4 (продолжение) Правило IfR ρ├ be ⇒B T ρ├ e ⇒A v ρ├
5. Семантика отношения ⇒B Правило CR Правило VarR Правило EqR ρ├ T ⇒B T ρ├ bx ⇒B
6. Семантика отношения ⇒B (продолжение) Правило BOpR Правило NotR ρ├ be ⇒B bv ρ├ be bop be’
7. Определение функций Введем новую синтаксическую категорию - имена функций. С этими именами будем связывать тела функций
9. Скачать презентацию

Слайд 2

Отношение ⇒ языка Exp4
Оно имеет две составляющие: арифметическую ρ├ e =>А v

и булеву ρ├ be =>B bv
Окружение в языке Exp4 определяется объединением двух функций ρ:Var∪BVar → Num∪{T,F}
Таким образом значения в окружении становятся типированными: ρ(x) ∈ Num, ρ(bx) ∈ {T,F}.
Типы отношений: =>А : ENV -> Exp4 -> Num =>B : ENV -> Bexp -> {T,F}.

Слайд 3

Естественная семантика языка Exp4
Правило CR
Правило VarR
Правило OpR
Правило LocR
ρ├ n ⇒A n
ρ├ e

⇒A v

ρ[x/v]├ e’ ⇒A v’

ρ├ let x = e in e’ ⇒A v’

ρ├ x ⇒A ρ(x)

ρ├ e ⇒A v

ρ├ e’ ⇒A v’

ρ├ e op e’ ⇒A Ap(opNum, v, v’)

Слайд 4

Естественная семантика языка Exp4 (продолжение)
Правило IfR
ρ├ be ⇒B T
ρ├ e ⇒A v
ρ├

if be Then e Else e’ ⇒A v

ρ├ be ⇒B F

ρ├ e’ ⇒A v’

ρ├ if be Then e Else e’ ⇒A v’

Слайд 5

Семантика отношения ⇒B
Правило CR
Правило VarR
Правило EqR
ρ├ T ⇒B T
ρ├ bx

⇒B ρ(bx)

ρ├ e ⇒A v

ρ├ e’ ⇒A v

ρ├ Equal(e,e’) ⇒B T

ρ├ F ⇒B F

ρ├ e ⇒A v

ρ├ e’ ⇒A v’

ρ├ Equal(e,e’) ⇒B F

[v =/= v’]

Слайд 6

Семантика отношения ⇒B (продолжение)
Правило BOpR
Правило NotR
ρ├ be ⇒B bv
ρ├ be bop

be’ ⇒B Ap(bop, bv, bv’)

ρ├ be’ ⇒B bv’

ρ├ be ⇒B T

ρ├ Not be ⇒B F

ρ├ be ⇒B F

ρ├ Not be ⇒B T

Слайд 7

Определение функций
Введем новую синтаксическую категорию - имена функций. С этими именами

будем связывать тела функций и таким образом делать определения.
Например,
square(x) <= x*x.
Такое определение будем называть декларацией.
Смысл выражения square(3) можно сформулировать так: «Вычислить x*x в окружении, где с x связано 3» . Обобщённо в форме правила: Если задана декларация f(x)<=e, то применимо правило:

ρ├ e’ ⇒ v’

ρ[x/v’]├ e ⇒ v

ρ├ f(e’) ⇒ v