# Tagged Questions

The tag has no usage guidance.

31 views

### Program equivalence with Structural induction

I recently attended my first lecture on structural induction and the professor stated that structural induction can be used to to prove that two programming languages are equivalent. I am new to ...
36 views

### How does the induction proof work in this example?

Refer to answer 1.1 of this file: http://www.dei.unipd.it/~geppo/AA/DOCS/NPC.pdf From my understanding and this thread, http://math.stackexchange.com/a/928412, we need 3 steps for that proof. ...
32 views

### Structural induction hypothesis on derivations

I am relatively new to the field of language semantics, however i am a bit confused about using operational semantics and structural induction on Derivations. If I have two languages $L1$ and $L2$ and ...
64 views

### Lambda Calculus inductive substitution definition

I'm reading Lambda-Calculus and Combinators: An Introduction, and there's the following definition of $\lambda$-substitution: $FV(P)$ stands for the set containing all free-variables from $P$. I ...
82 views

### How to use the concept of loop invariant to reduce errors in loops?

Most of time while writing loops I usually write wrong boundary conditions(eg: wrong outcome) or my assumptions about loop terminations are wrong(eg: infinitely running loop). Here is an small example ...
20 views

### Why do I need a base case for n=3 when solving a d&c recurrence?

I was reading CLRS' book on how to use the substitution method to solve recurrences, where they have the following example: $T(n) = 2T(\lfloor{\frac{n}{2}}\rfloor) + n$ where $T(1) = 1$ They assume ...
24 views

### How would one prove that the following scheme definition is an ordered stream of integers

How would one prove that the following scheme definition is an ordered stream of integers (define integers (cons-stream 1 (add-streams ones integers)))
35 views

### simple iterate algorithm proof by induction

Suppose I have a function where it calculates which bit is larger called LargerBinary. Let's say I have an input 110111;101001, the output will be 110111 and if the input is 110110:110110, the output ...
82 views

### proof using induction of automaton

How I can explain this. Consider the following automaton, $A$. Prove using the method of induction that every word/string $w\in L(A)$ contains an odd number(length) of $1$'s. Show that there are ...
53 views

### Structural induction on generic list

In preparation for an exam, I've come upon the following problem. Given the constructors : ...
65 views

### Prove by induction that the running time of recursive Fibonacci is exponential

This example followed from a Fibonacci algorithm in class. The professor showed us how to compute $T(n) = T(n-1) + T(n-2) + 3$, but left this step for us to prove, so I decided to attempt to prove it! ...
75 views

### Prove correctness of recursive algorithm

I have this java function: ...
60 views

### Proving that the reversal of a language reversal is that language

I am trying to prove that with language L, (L^R) ^R =L So that the reversal of the reversal of the language is the original language L. I have proved that before with a string not language (let's ...
65 views

### Substituting two different identifiers with the same identifier in Coq - why does this work?

I'm playing around with Coq and Software Foundations and is somehow very confused by something I took for granted since forever. To prove ...
74 views

55 views

43 views

### Prove by Induction that $r_n$ is $O(\log_2(\log_2n))$ [duplicate]

Let the sequence $r$ be defined by: \begin{align*}r_{1} &= 1\\ r_n&= 1 + r_{\lfloor\sqrt{n}\rfloor}\,,\quad n\geq 2\,.\end{align*} Prove by induction that $r_n$ is $O(\log_2(\log_2n))$. ...
197 views

### Structural induction over list

I want to prove that unique(reverse(L)) = reverse(unique(L)) where L is a List. List has the following constructors: ...
78 views

### Pierce's Types and Programming Languages : circular definition of terms?

In Pierce's book, on page 26-27 it is given a definition of terms for a simple language using inference rules. In the picture below it is marked by red highlighting the problematic part. What is ...
114 views

247 views

### Proof of big theta using induction [duplicate]

Here is a recursive definition for the runtime of some unspecified function. $a$ and $c$ are positive constants. $T(n) = a$, if $n = 2$ $T(n) = 2T(n/2) + cn$ if $n > 2$ Use induction to prove ...
57 views

### Using induction to prove transition states are the same

Suppose that you have a DFA $M=\left(S,\Sigma,s_0,\delta,{s_f}\right)$ with $s_f\neq s_0$. Suppose further that, for all $a\in\Sigma$, $\delta\left(s_0,a\right)=\delta\left(s_f,a\right)$. Show that ...
283 views

### Is path induction constructive?

I'm reading through the HoTT book and I have a hard time with path induction. When I look at the type in the section 1.12.1: \text{ind}_{=_A}:\prod_{C:\prod\limits_{x,y:A}(x=_Ay)\to \mathcal{U}} \...
415 views

236 views

### How to apply the substitution method to n/2?

I recently was introduced to solving recurrence bounds by substitution but there's something i don't understand about it. In standard induction proofs you prove a base case, assume it holds for n ...