Řešení

Řádný termín

Vytvor datovy typ na reprezenaciu lambda kalkulu a napis funkciu pre beta redukciu
Napis funkciu, ktora zo zoznamu urobi zoznam zoznamov (z [1,2,3] spravi [[1],[2],[3]]) a dokaz funkcnost pomocou map. Indukcny predpoklad sme mali vymysliet na mieste.
Napis funkciu, ktora otvori 2 zadane subory, v prvom skontroluje, ci obsahuje vyraz aⁿbⁿbⁿ. Ak ano, do druheho suboru zapis n, ak nie, vypis na stdout „Error“ a do druheho suboru zapis poziciu chyby. Boli zadane funkcie na pracu so subormi.

import System.IO
 
-- 1
 
data LC a
	= Var a
	| App (LC a) (LC a)
	| Abs a (LC a)
	deriving (Show, Eq, Read)
 
betared :: Eq a => (LC a) -> (LC a) -> (LC a)
betared (Abs a body) ex = subst [] body
	where
		fvex = fv ex
		subst bnds (Var v)
			| v /= a = Var v
			| foldr (||) False (map (\x -> x `elem` bnds) fvex) = error "Free variable occurs bound in the beta reduction"
			| True = ex
		subst bnds (App e1 e2) = App (subst bnds e1) (subst bnds e2)
		subst bnds abs@(Abs x ex) = if x == a then abs else Abs x (subst (x:bnds) ex)
betared _ _ = error "Just lambda-abstraction can be applied"
 
fv (Var x) = [x]
fv (App e1 e2) = fv e1 ++ fv e2
fv (Abs v body) = filter (/= v) $ fv body
 
 
-- 2
 
lister l = map' f l			-- /1
	where
		f x = [x]		-- /2
 
map' f (x:xs)	= f x : map' f xs	-- /3
map' _ _	= []			-- /4
 
{-
 
1)
Chci dokázat:
lister [] = []
====
	lister []
=|1	map' f  []
=|4	[]
 
 
2)
I.H.: lister as = ass
 
Chci dokázat:
lister (a:as) = [a] : ass
====
	lister (a:as)
=|1	map' f (a:as)
=|3	f a : map' f as
=|1	f a : lister as
=|IH	f a : ass
=|2	[a] : ass
 
Q.E.D.
 
 
2] vartiantní přístup
I.H.: lister as = [[a1], ..., [an]]
 
Chci dokázat:
lister (a:as) = [[a],[a1], ..., [an]]
===
	lister (a:as)
=|1	map' f (a:as)
=|3	f a : map' f as
=|1	f a : lister as
=|IH	f a : [[a1], ..., [an]]
=|2	[a] : [[a1], ..., [an]]
=|def(:)	[[a],[a1], ... , [an]]
 
Q.E.D.
 
-- pozn: bylo možno uvést i definici (:) a [], ale to je zbytečné
-- pozn2: uznal jsem i definici s lister [] = [] i když potom byly všechny důkazy na něm založené špatně
-}
 
 
-- 3
 
fabc fi fo = do
	hi <- openFile fi ReadMode
	ho <- openFile fo WriteMode
	ct <- hGetContents hi
	let (res, val) = proc ct
	hPutStr ho (show val)
	if res then return () else hPutStr stderr "Error"
	hClose ho
	hClose hi
 
proc l
	| las == lbs && lbs == lcs && (length nocs == 0) = (True, las)
	| True = (False, err)
	where
		(als, noas) = span (== 'a') l
		las = length als
		--
		(bs, nobs) = span (== 'b') noas
		lbs = length bs
		--
		(cs, nocs) = span (== 'c') nobs
		lcs = length cs
		--
		err
			| las == 0 = 1
			| las == lbs = if lcs > las then las + las + las + 1 else las + las + lcs + 1
			| True = if lbs > las then las + las + 1 else las + lbs + 1
 
 
-- span f l = (takeWhile f l, dropWhile f l)
-- pozor! takeWhile (=='a') a filter (=='a') není to samé!!!
 
-- EOF

Napis predikat ktory pre sachovnicu zadanych rozmerov a 2 zadanych pozicii urci pocet acyklickych grafov, ktore zacinaju v prvom bode, prejdu druhym a vratia sa znovu do prveho
???
Napis predikat substr(Str,Sub), ktory urci, ci Sub je podretazcom Str

reseniRadna.pl

:- dynamic posx/2, sizeX/1, sizeY/1.
 
 
/* 1 */
 
numofp(X1, Y1, X1, Y1, XS, YS, 1)
	:-	XS > 1, YS > 1,
		retractall(sizeX(_)), retractall(sizeY(_)), assert(sizeX(XS)), assert(sizeY(YS)),
		testX(X1),
		testY(Y1),
		!.
numofp(X1, Y1, X2, Y2, XS, YS, NUM)
	:-	XS > 1, YS > 1,
		retractall(sizeX(_)), retractall(sizeY(_)), assert(sizeX(XS)), assert(sizeY(YS)),
		testX(X1), testX(X2),
		testY(Y1), testY(Y2),
		retractall(posx(_, _)),
		setof(RR, search(X1, Y1, X1, Y1, RR), RES),
		fltr(RES, (X2:Y2), RX), length(RX, NUM).
 
 
search(X, Y, X, Y, [(X:Y)])
	:-	posx(_, _), !.
search(X1, Y1, X2, Y2, [(X1:Y1)|P])
	:-	assert(posx(X1, Y1)),
		move(X1, Y1, XN, YN),
		(not(posx(XN, YN)); (X2 = XN, Y2 = YN)),
		search(XN, YN, X2, Y2, P).
search(X1, Y1, _, _, _)
	:-	posx(X1, Y1),
		retract(posx(X1, Y1)),
		!, fail.
 
fltr([L|LS], V, [L|LX]) :- member(V,L), !, fltr(LS, V, LX).
fltr([_|LS], V, LX) :- fltr(LS, V, LX).
fltr([], _, []).
 
move(X, Y, NX, NY) :-
	NX is X + 1,
	NY is Y + 2,
	testX(NX),
	testY(NY).
move(X, Y, NX, NY) :-
	NX is X - 1,
	NY is Y + 2,
	testX(NX),
	testY(NY).
move(X, Y, NX, NY) :-
	NX is X + 1,
	NY is Y - 2,
	testX(NX),
	testY(NY).
move(X, Y, NX, NY) :-
	NX is X - 1,
	NY is Y - 2,
	testX(NX),
	testY(NY).
 
move(X, Y, NX, NY) :-
	NX is X + 2,
	NY is Y + 1,
	testX(NX),
	testY(NY).
move(X, Y, NX, NY) :-
	NX is X - 2,
	NY is Y + 1,
	testX(NX),
	testY(NY).
move(X, Y, NX, NY) :-
	NX is X + 2,
	NY is Y - 1,
	testX(NX),
	testY(NY).
move(X, Y, NX, NY) :-
	NX is X - 2,
	NY is Y - 1,
	testX(NX),
	testY(NY).
 
testX(X) :- sizeX(XX), X >= 1, X =< XX.
testY(Y) :- sizeY(YY), Y >= 1, Y =< YY.
 
/* 2 */
mapst(Map, Key, Value) :- nonvar(Map), var(Value), nonvar(Key), Get =.. [Map, Key, Value], call(Get).
mapst(Map, Key, Value) :- nonvar(Map), nonvar(Value), nonvar(Key), insrt(Map, Key, Value).
mapst(Map, Key, Value) :- nonvar(Map), nonvar(Value), var(Key), Get =.. [Map, K, Value], setof(K, Get, Key).
 
insrt(Map, Key, _) :- Test =.. [Map, Key, _], call(Test), !, fail.
insrt(Map, Key, Val) :- Asrt =.. [Map, Key, Val], assert(Asrt).
 
/* !!!!!!!!!!!!! NNEEEEE!!!! !!!!!!!!!!!!!! */
/* 2 BRUTUS chyby !!!!!!!!!!! */
 
mapstx(Map, _, _) :- var(Map), !, fail.
mapstx(_, Key, Value) :- var(Key), var(Value), !, fail.
mapstx(Map, Key, Value) :- var(Value), P =.. [Map, Key, Value], call(P).
mapstx(Map, Key, Value) :- var(Key), P =.. [Map, K, Value], setof(K, P, Key).
mapstx(Map, Key, Value) :- P =.. [Map, Key, Value], call(P), !, fail.
mapstx(Map, Key, Value) :- P =.. [Map, Key, Value], assert(P).
 
 
/* 3 */
 
sbstr([], []).
sbstr(Str, SStr) :- appnd(_, SStr, L), appnd(L, _ ,Str).
 
appnd([], L2, L2).
appnd([H|T], L2, [H|AP]) :- appnd(T,L2,AP).
 
 
/* 3 alternativa */
 
sbstr2([], []).
sbstr2([_|_], []).
sbstr2([H|T1], [H|T2]) :- prfx(T1, T2).
sbstr2([_|T], X) :- sbstr2(T, X).
 
prfx(_, []).
prfx([H|T1], [H|T2]) :- prfx(T1,T2).
 
 
/* !!!!!!!!!!!!! NNEEEEE!!!! !!!!!!!!!!!!!! */
/* zkuste varianty pro sbstrx([1,2,3],X). */
 
sbstrx(Str, Sub) :- sstr(Str, Sub, Sub).
 
sstr([H1|T1], [H2|T2], S) :- (H1 = H2 -> sstr(T1, T2, S); sstr(T1, S, S)).
sstr(_, [], _).
 
/* ---------------------- Goedel ----------------------- */
/*
 
MODULE PRIME.
IMPORT Integers.
 
PREDICATE Prime : Integer.
 
Prime(prime) <- ~ SOME [x] (x > 1 & x < prime & prime Mod x = 0).
 
*/
/* ---------------------- Goedel ----------------------- */
 
/* EOF */

1. opravný termín

eq v lambda kalkulu
unlister [[1], [2], [3]] → [1, 2, 3] (nedefinovane chovani pro viceprvkove vnitrni seznamy) + dukaz
Zalamat text na dany pocet znaku na radek

resOprava1.hs

import IO
 
{- ------------ (1) ------------
 
lambda kalkul
 
LET True = λxy.x
LET False = λxy.y
 
LET eq = λab.iszero(a prev b) (iszero(b prev a)) False
 
Jelikoz cisla jsou definovana takto:
 
LET 0 = λfn.n
LET N = λfn.f^N n
 
neexistuje zaporne cislo!!! Tedy test musel byt obousmerny.
Tedy reseni s jednim smerem je na nic.
 
Pokus o rekurzi v definici odporuje primo lambda kalkulu.
Taky zadne body.
 
-}
 
 
{- ------------ (2) ------------ -}
 
unlister l = _foldr f [] l		-- 1
	where
		f [x] xs = x:xs		-- 2
 
_foldr _ a [] = a			-- 3
_foldr f a (x:xs) = f x (_foldr f a xs)	-- 4
 
{-
Pro []
 
unlister []
=|1	_foldr f [] []
=|3	[]
 
 
I.H.
unlister [[x1], ..., [xn]] = [x1, ..., xn]
 
Pro
	as = [[x1], ..., [xn]]
	a = [x0]
 
unlister (a:as)
=|1	_foldr f [] (a:as)
=|4	f a (_foldr f [] as)
=	f [x0] (_foldr f [] [[x1], ..., [xn]])
=|1	f [x0] (unlister [[x1], ..., [xn]])
=|IH	f [x0] [x1, ..., xn]
=|2	[x0, x1, ..., xn]
 
Q.E.D.
-}
 
 
{- znacne pracnejsi reseni s (++) -}
 
unlister' l = _foldr (++) [] l		-- 5
 
{-
 
Je nutne uvest definici (++) !!!!!
 
(++) [] ys = ys				-- 6
(++) (x:xs) ys = x:(xs ++ ys)		-- 7
 
 
Pro []
 
unlister' []
=|5	_foldr (++) [] []
=|3	[]
 
 
I.H.
unlister' [[x1], ..., [xn]] = [x1, ..., xn]
 
Pro
as = [[x1], ..., [xn]]
a = [x0]
 
unlister' (a:as)
=|5	_foldr (++) [] (a:as)
=|4	(++) a (_foldr (++) [] as)
=	(++) [x0] (_foldr (++) [] [[x1], ..., [xn]])
=|5	(++) [x0] (unlister' [[x1], ..., [xn]])
=|IH	(++) [x0] [x1, ..., xn]
=|7	x0 : ([] ++ [x1, ..., xn])
=|6	x0 : [x1, ..., xn]
=|:	[x0, x1, ..., xn]
 
-}
 
 
shrink n fi fo = do
	hi <- openFile fi ReadMode
	ho <- openFile fo WriteMode
	cont <- hGetContents hi
	hPutStr ho $ unlines $ concat $ map (shrinkP n) $ par $ lines cont
	hClose ho
	hClose hi
 
par ls
	| null rst = [concat p1]
	| null p1 = [concat nosp]
	| True = concat p1 : par rst
	where
		nosp = dropWhile (== []) ls
		(p1, rest) = span (/= []) nosp
		rst = dropWhile (== []) rest
 
shrinkP _ [] = []
shrinkP width cs
	| null wds = [cs, ""]
	| True = join (head wds) (tail wds)
	where
		wds = words cs
		join l (w:ws)
			| length l + 1 + length w > width = l : join w ws
			| True = join (l ++ (' ':w)) ws
		join l [] = [l, ""]
 
 
-- EOF

Najit vsechny cesty na sachovnici, ktere nejakym polickem projdou prave dvakrat
Nejaky strom
Otoci „slova“ v seznamu ([1, 2, 3, 0, 1, 2, 3] → [3, 2, 1, 0, 3, 2, 1], 0 je „mezera“)

resOprava1.pl

/* 1 */
 
:- dynamic ps/2, cycle/2.
:- dynamic sizeY/1, sizeX/1.
 
findall(X1, Y1, X2, Y2, SX, SY, RES) :-
	SX > 0, SY > 0,
	retractall(sizeX(_)), retractall(sizeY(_)),
	assert(sizeX(SX)), assert(sizeY(SY)),
	testP(X1, Y1), testP(X2, Y2),
	retractall(ps(_, _)), retractall(cycle(_, _)),
	setof(R, search(X1, Y1, X2, Y2, R), RES).
 
testP(X, Y) :-
	X > 0, Y > 0,
	sizeX(XX), X =< XX,
	sizeY(YY), Y =< YY.
 
search(X, Y, X, Y, [X:Y]) :- cycle(_, _), !.
search(X, Y, X, Y, _) :- not(cycle(_, _)), !, fail.
search(X, Y, XX, YY, [X:Y|R]) :-
	cycle(_, _),
	assert(ps(X, Y)),
	nxtStep(X, Y, NX, NY),
	not(ps(NX, NY)),
	search(NX, NY, XX, YY, R).
search(X, Y, XX, YY, [X:Y|R]) :-
	not(cycle(_, _)),
	assert(ps(X, Y)),
	nxtStep(X, Y, NX, NY),
	tryTwo(NX, NY),
	search(NX, NY, XX, YY, R).
search(X, Y, _, _, _) :-
	ps(X, Y), not(cycle(X, Y)),
	!, retract(ps(X, Y)),
	fail.
 
tryTwo(NX, NY) :-
	ps(NX, NY),
	assert(cycle(NX, NY)).
tryTwo(NX, NY) :-
	cycle(NX, NY),
	!, retract(cycle(NX, NY)),
	fail.
tryTwo(NX, NY) :-
	not(ps(NX, NY)).
 
nxtStep(X, Y, XX, Y) :-
	sizeX(SX), X < SX,
	XX is X + 1.
nxtStep(X, Y, XX, Y) :-
	XX is X - 1,
	XX > 0.
nxtStep(X, Y, X, YY) :-
	sizeY(SY), Y < SY,
	YY is Y + 1.
nxtStep(X, Y, X, YY) :-
	YY is Y - 1,
	YY > 0.
 
/* 2 */
 
emptyT(leaf).
 
insval(V, leaf, node(V, leaf, leaf)).
insval(V, node(W, L, R), node(W, LL, R)) :-
	V < W, insval(V, L, LL).
insval(V, node(W, L, R),node(W, L, RR)) :-
	V > W, insval(V, R, RR).
insval(V, node(V, L, R), node(V, L, R)).
 
l2t([], leaf).
l2t([H|T], R) :-
	l2t(T, TR),
	insval(H, TR, R).
 
t2l(leaf, []).
t2l(node(V, L, R), ResL) :-
	t2l(L, LL),
	t2l(R, RL),
	append(LL, [V|RL], ResL).
 
tree2list(T, L) :-
	var(T), var(L), !, fail.
tree2list(T, L) :-
	var(T), l2t(T, L).
tree2list(T, L) :-
	var(L), t2l(T, L).
tree2list(T, L) :-	/* tady to slo ruzne, nic neni 100% */
	nonvar(L), nonvar(T),
	t2l(T, LL), LL = L.
 
/* 3 */
 
/* takovy trochu Haskell v Prologu */
 
revin([], _, []).
revin([H|T], S, RES) :-
	words([H|T], S, WRDS),
	revall(WRDS, REV),
	unwords(REV, S, RES).
 
words([], _, []).
words([H|_], H, _) :-
	!, fail.	/* an error */
words([H|T], S, [[H|W]|WS]) :-
	inw(T, S, x(W, R)),
	words(R, S, WS).
 
inw([], _, x([], [])).
inw([H|T], H, x([], T)) :- !.
inw([H|T], S, x([H|W], R)) :-
	inw(T, S, x(W, R)).
 
revall([L|LS], [RL|RLS]) :-
	reverse(L, RL),
	revall(LS, RLS).
revall([], []).
 
unwords([], _, []).
unwords([L|LS], _, L) :-
	nll(LS), !.
unwords([L|LS], S, UR) :-
	append(L, [S], LSP),
	unwords(LS, S, UW),
	append(LSP, UW, UR).
 
nll([]).
nll([_|_]) :- !, fail.	/* je ale zbytecny */
 
/* brutus Prolog */
/* inspirace v pisemece, upraveno pro spravnou funkcnost */
 
revn([], _, []).
revn(Str, Spc, Res) :-
	not(member(Spc, Str)), !,
	reverse(Str, Res).
revn(Str, Spc, Res) :-
	append(L, [Spc|Rest], Str),
	not(member(Spc, L)), !,
	reverse(L, RL),
	revn(Rest, Spc, InRes),
	append(RL, [Spc|InRes], Res).
 
/*
 
member(H,[H|_]).
member(X,[_|T]) :- member(X,T).
 
*/
 
/* EOF */