- The following is an ML program that computes the factorial function.
It uses a locally defined function to do this computation.
fun fact n = let fun aux(0,acc) = acc | aux(m,acc) = aux(m - 1,m * acc) in aux(n,1) end;

Write a lambda Prolog program in the style of the one for`reverse`given in Figure 5.15 that implements the factorial relation using a locally defined auxiliary predicate. - The following is an ML program that computes the Fibonacci program.
It uses a locally defined function to do this computation.
local fun iter(this,prev:int,count,n) = if count = n then this else iter(this+prev,this,count+1,n); in fun fib 0 = 0 | fib n = iter(1,0,1,n); end;

Write a lambda Prolog program in the style of the one for`reverse`given in Figure 5.15 that implements the Fibonacci relation using such a locally defined auxiliary predicate. - Which of the following formulas are provable and which are not?
Attempt to verify this by hand before asking lambda Prolog to verify
your conclusions.
pi x\(sigma y\( p x => p y)). sigma x\(pi y\( p x => p y)). pi x\(pi y\(q x y => pi z\(q x z))). pi x\(sigma y\(q x y => pi z\(q x z))). sigma x\(pi y\(q x y => pi z\(q x z))). pi x\(pi y\(q x y => sigma z\(q x z))). (pi x\(pi y\(p x => q x y))) => pi x\(p x => pi y\(q x y)). (pi x\(p x => pi y\(q x y))) => pi x\(pi y\(p x => q x y)).

Lectures / Modules / Homeworks / Syllabus