View file src/slc/rep.prf - Download

# Representation of proofs and evaluation of representations
#
# Run Proof Logic with option -f for full reduction
# Example :
# $ rlwrap ./pl-v10 -f
# 
# data Proof =
#    SMB String 
#  | VAR
#  | NXV Proof
#  | FNC Proof
#  | APL Proof Proof
#  | GTR Proof Proof
#  | EQU Proof Proof

# & B ^f ^g ^x (f (g x)).
# & M [* *].
# & Y ^f (M (B f M)).

& Y [[* *] ['* (* *)]]. 
///(Y f) ; f //(Y f).

& SMB ^name ^s ^v ^n ^f ^a ^t ^e (s name).
& VAR ^s ^v ^n ^f ^a ^t ^e v.
& NXV ^x ^s ^v ^n ^f ^a ^t ^e (n x).
& FNC ^x ^s ^v ^n ^f ^a ^t ^e (f x).
& APL ^x ^y ^s ^v ^n ^f ^a ^t ^e (a x y).
& GTR ^x ^y ^s ^v ^n ^f ^a ^t ^e (t x y).
& EQU ^x ^y ^s ^v ^n ^f ^a ^t ^e (e x y).

& evalv (Y ^eva ^v ^x (x
 ^name name
 v
 ^x '(eva v x)
 ^x [eva * x]
 ^x ^y (eva v x (eva v y))
 ^x ^y (eva v x ; eva v y)
 ^x ^y (eva v x = eva v y)
)).
 
& eval (evalv *).

~(eval (SMB a)).
~(eval VAR).
~(eval (NXV VAR)).
~(eval (FNC VAR)).
~(eval (FNC (SMB a))).
~(eval (APL (SMB a) (SMB b))).
~(eval (GTR (SMB a) (SMB b))).
~(eval (EQU (SMB a) (SMB b))).