Пример вычисления выражений на КАМ

Рекурсия в КАМ

Дополнительные функциональные инструкции

Оптимизация кода КАМ

Два вида оптимизации:

переход к многоместным операциям, т.е. вместо функции “+”, которая будет брать аргументы по очереди, рассмотрим двуместный “+”.

а) App○< App○<’+,x>,y> = +<x,y>

б) Воспользуемся категориальным равенством для β-редукции.

App○<Λ(х)○у, z> = x○<y,z>

{(λx.y)z→[z/x]y – соответствующее категориальное равенство.}

Терм	Код	Стек	Терм	Код	Стек
True	If a b c	sm	S	a c	m
False	If a b c	sm	S	b c	m
(a,b)	add c	S	{a+b}^н. число	C	S
(a,b)	eq C	S	True/False	C	S

Пример. push quote 2 swap quote 3 cons add(пример сложения 2 и 3).

Две инструкции: dum c,wind c.

Терм	Код	Стек	Терм	Код	Стек
t	dum c	S	$Y	C	S
[a:b]	wind c	(t$Y)S	(t.[a:b])	C	S

wind – аппликация для работы с объектами (вида D) – рекурсивными

Схема трансляции терма расширенного λ-исчисления в код КАМ

lambda x M→(cur[M](ρ,x))

^(λx.M) M транслируется в среде ρ, расширенной переменной х.

app AB→(push)|[A]ρ|(swap)|[B] ρ|(cons app)

| - слияние списков

(ab)|(cde) → (abcde)

[ ] - транслирование в среде.

_{↓подстановка}

let x=M in N →(push)|[M]ρ|(cons)|[N](ρ,x)

_{↓рекурсивная}

letrec x=M in N→(push dum cons push)|[M](ρ,x)|(wind)|[N](ρ,x)

quote c→(quote c)

cons AB→(push)|[A]ρ|(swap)|[B]ρ|(cons)

Fst A→[A]ρ|(Fst)

Snd A→[A]ρ|(Snd)

If C A B→(push)|[C]ρ|(if [A]ρ[B]ρ)

eq A B→(push)|[A] ρ|(swap)|[B]ρ|(cons eq)

+AB→(push)|[A] ρ|(swap)|[B]ρ|(cons add)

*AB→(push)|[A] ρ|(swap)|[B]ρ|(cons mult)

Переменные получаются из среды с помощью композиции операций Fst и Snd.

Пример. ((lambda x(+x1))3)]()

Начинаем транслировать в пустой среде:

[((lambda x (+x1))3)]()

Транслируем аппликацию:

(push)|[lambda x (+x1))]()|(swap)|[3]()|(cons app)

трансляция [3]() → quote 3

(push)|[(lambda x (+x1))]()|(swap quote 3 cons app)

среда для трансляции (+х1) расширилась до ((),x):

(push)|(cur [+x1]((),x))|(swap quote 3 cons app)

(push cur [+x1]((),x)swap quote 3 cons app)

транслируем сложение

(push cur(push|[x]((),x)|(swap)|[1]((),x)|(cons add))swap quote 3 cons app

(push cur(push Snd swap quote 1 cons add)swap quote 3 cons app)

App○<x,y>=<x,y>App

Пример. (λх.х4((λх.х)3))+

App○< Λ(App○<App○<App<Snd,'4>,App○< Λ(Snd),'3>>),'+>

Терм	Код	Стек
()	<Λ(<<Snd,'4>app,<Λ(Snd),'3>app>app),'+>app	[ ]
()	Λ(<<Snd,'4>app,<Λ(Snd),'3> └──A────┘└──B─── app^‫ >app),'+>app	()
[<A,B>app:()]	, Λ(Snd'+)>app	()
()	Λ(Snd'+)>app	[<A,B>app:()]
[Snd'+;()]	>app	[<A,B>app:()]
[<A,B>app:()], [Snd'+;()]	app	[ ]
((),[Snd'+:()])	<A,B>app	[ ]
((),[Snd'+:()])	A,B>app	((),[Snd'+:()])
((),[Snd'+:()])	Snd,'4>app,B>app	((),[Snd'+:()]);((),[Snd'+:()])
[Snd'+:()]	,'4>app,B>app	((),[Snd'+:()]);((),[Snd'+:()])
((),[Snd'+:()])	'4>app,B>app	[Snd'+:()];((),[Snd'+:()])
	>app,B>app	[Snd'+:()];((),[Snd'+:()])
([Snd'+:()],4)	app,B>app	((),[Snd'+:()])
((),4)	Snd'+,B>app	((),[Snd'+:()])
	+,B>app	((),[Snd'+:()])
{+ 4}	,B>app	((),[Snd'+:()])
((),[Snd'+:()])	B>app	{+ 4};((),[Snd'+:()])
((),[Snd'+:()])	Λ(Snd),'3>app>app	((),[Snd'+:()]);{+ 4}
(Snd:(),[Snd'+:()]))	,'3>app>app	((),[Snd'+:()]);{+ 4}
((),[Snd'+:()])	'3>app>app	(Snd:(),[Snd'+:()])) + 4
	>app>app	(Snd:(),[Snd'+:()])) + 4
[(Snd: ((),[ ])),3]	app>app	+ 4
[((),[Snd'+: ()]),3]	Snd>app

Вычислим факториал на КАМ

ƒact 1

ƒact x: if x=0 then 1 else x* ƒact(x-1)

ƒact 1:[letrec [ ƒac=λx.if(eq x’0)’1(*x(app ƒac(-x’1)))] in (app ƒac’1) ] ()

(push dum cons push)|[ λx. if(eq x’0)’1 (*x(app ƒac(-x’1)))](().ƒac)|(wind)|[(app ƒac’1)] (().ƒac)

(push dum cons push)|(cur[if(eq x’0)’1 (*x(app ƒac(-x’1)))](().ƒac)|(wind)|

|(push)|[ ƒac]((). ƒac)|(swap)|[‘1]((). ƒac)|(cons app)

_{↓начало каррирования}

(push dum cons push cur((push)|[(eq x'0)]((().ƒac).x)|(if [1’]((().ƒac).x)[(*x(app

ƒac (-x’1)))]((().ƒac)x.)) wind push snd swap quote 1 cons app)

^{↑закончилось каррирование}

(push dum cons push cur^|((push)|(push) Snd swap quote 0 cons eq)|

|(if (quote 1)(push snd swap)|[app ƒac(-x’1))]((().ƒac).x)|(cons mult)))^| wind push

snd swap quote 1 cons app)

Оттранслируем аппликацию:

(push)|[ ƒac](((). ƒac).x)|(swap)|[(-x’1)](((). ƒac).x)|(cons app)→(push Fst Snd swap push Snd swap push Snd swap quote 1 cons sub cons app)

Подставляем это выражение и получаем окончательный результат:

(push dum cons push cur^|(push push snd swap quote 0 cons eq if (quote 1)(push Snd swap push Fst Snd swap push Snd swap quote 1 cons sub cons app cons mult))^|

wind push Snd swap quote 1 cons app)

В сокращенном виде:

↓_wind

<Y><Λ^|(<<S,’0>=if(‘1)(<S,<FS,<S,’1>->app>*))^|appY<S,’1>app)

↑^{cпециальная аппликация для Y}

На каждом этапе транслировались самые внешние выражения.

Контрольные вопросы

1. Какие способы избавления от имен переменных Вы знаете?
2. Выпишите семантические равенства для категориальной комбинаторной логики
3. Какое из семантических равенств ККЛ позволяет вводить константы?
4. Назовите два способа получения кода КАМ для λ–выражения.
5. Получите двумя способами КАМ-код для выражения (λxy.+ x y)7((λx.x)12) и вычислите его средствами абстрактной машины.
6. Воспользовавшись приведенным кодом, вычислите на КАМ факториал 2.

Дата добавления: 2014-01-11