Online Otter-λ

Utility Link | Utility Link | Utility Link
ExternalSimplification | SetTheory | LambdaLogic | Induction | More >
-->

Examplessmall logo



Examples -> LambdaLogic -> lambda.in


% test file for lambda and ap.
% Demonstrates beta reduction and renaming of bound variables to avoid capture.

set(lambda).
set(demod_inf).
set(binary_res).

list(usable).
x = x.
end_of_list.

list(demodulators).
x *x = x.
end_of_list.

list(sos).
ap(ap(lambda(x,lambda(y,x)),c*c),y) != c | % beta reduction works fine combined with ordinary demodulation
ap(lambda(x,lambda(y,x)),y) != lambda(z,y) | % y will not be captured in the beta-reduction
lambda(x,x) != lambda(z,z) | % these two differ by renaming a bound variable
lambda(z,a) != lambda(z,x) | % succeeds with x:= a
lambda(w,a) != lambda(z,x). % also succeeds with x:= a
end_of_list.

% Note: lambda(x,a) != lambda(z,x) would be illegal input, since x occurs both free and lambda-bound in the same clause.
% The bound x would have to be renamed first.