Let (F_n^')n in N be the family of terms defined by induction on n in N as follows: F_0^', F_{n+1}^{'}=c underline{n+1} F_n^'

steveo963200054

steveo963200054

Answered question

2022-09-04

Proving terms using induction in LC
Let ( F n ) n N be the family of terms defined by induction on n N as follows:
F 0 = m F n + 1 = c n + 1 _ F n
where c and m are variables, and n _ is the Church numeral representing n N .
I'm trying to prove by induction on n N that
F n [ t i m e s / c , 1 _ / m ] β n ! _
and thus, by setting F n = λ c . λ m . F n ,
F n t i m e s 1 _ β n ! _
where ! is factorial, and times is a term such that timesa–– t i m e s a _ b _ β a × b _ for any a , b N . How can I do it?

Answer & Explanation

Adrienne Harper

Adrienne Harper

Beginner2022-09-05Added 14 answers

Step 1
It is possible to prove that, for every n N , we have F n [ t i m e s / c , n _ / m ] β n ! _ , by straightforward induction on n N .
- Base case n = 0: By definition, F 0 = m and so F 0 [ t i m e s / c , 1 _ / m ] = 1 _ = 0 ! _ (remember that 0 ! = 1), and so F 0 [ t i m e s / c , 1 _ / m ] β 0 ! _ because β is a reflexive relation.
- Inductive case: Given n N , we suppose that F n [ t i m e s / c , n _ / m ] β n ! _ (this is our inductive hypothesis) and we want to show that F n + 1 [ t i m e s / c , n + 1 _ / m ] β ( n + 1 ) ! _ . By definition, F n + 1 = c n + 1 _ F n and hence
F n + 1 [ t i m e s / c , n + 1 _ / m ] = t i m e s n + 1 _ ( F n [ t i m e s / c , n _ / m ] ) β t i m e s n + 1 _ n ! _ (by inductive hypothesis) β ( n + 1 ) × n ! _ (by definition of  t i m e s ) = ( n + 1 ) ! _
Step 2
So, we have proved that, for every n N ,
( ) F n [ t i m e s / c , n _ / m ] β n ! _
As a consequence, F n t i m e s 1 _ β n _ for every n N . Indeed,
F n t i m e s 1 _ = ( λ c . λ m . F n ) t i m e s 1 _ β ( λ m . F n [ t i m e s / c ] ) 1 _ β F n [ t i m e s / c , n _ / m ] β n ! _ (by  ( ) )

Do you have a similar question?

Recalculate according to your conditions!

New Questions in Discrete math

Ask your question.
Get an expert answer.

Let our experts help you. Answer in as fast as 15 minutes.

Didn't find what you were looking for?