oldchap9stuff.tex

  \subsubsection{Generalization / Specialization}
  
  One test of whether an interpretation has any value is whether it can be used to predict.
  Suppose we tentatively adopt the premise that students have trouble with generalization, and subsequent specialization, and with alternative representations of the same idea.
  
  Then, we would be able to predict the results of certain interactions on certain situations. Consider the situation that students are learning to produce programs starting from simple example procedures, and aggregating experience with procedures that helps them build more complicated examples, and combining, parts of procedures they have seen into larger programs.
  
  Hoping these students will generalize their experience with programs to the idea of programs in general, and then hoping that these students will be able to appreciate a component hierarchical decomposition of the idea of program such that managing the accessing (reading and writing) of data is a part and hoping the students will be able to generalize the managing of data to the idea of data structures, and hoping the students will appreciate an exposition of multiple alternative data structures, is making use of generalization and specialization that might not yet be strengths the students have.
  
  If generalization from examples and specialization to novel examples is difficult for students, we could predict that they would find data structures demanding of effort.
  
  If generalization from one representation, such as graphical representation of a tree, to the idea of relation, and specialization of representation of that relation to use of attributes in a class that are references to instances is difficult, then we could predict that students would not know how to implement a tree structure in code, even if they felt they ``knew the principle'' as shown in a graph.
  
  With respect to argumentation, we would like to know whether the argument is always being noticed, or whether there is a conceptualization that the argument may be ignored, because the conclusion is checked by some other means (such as, the student regards the conclusion as obvious).
  
  It might be helpful to try to distinguish between the understanding of argument vs. the process of generalization, as a source of difficulty in advancing from recognizing the correctness of a conclusion of an argument whose free variables have been bound to concrete entities to recognizing an argument form as persuasive.
  
  We might, for example, discuss an argument populated with concrete entities, about the (true) conclusion of which, students are in agreement. We might ask why they know the conclusion is true. We might discover whether the argument is given as the reason.
  
  We would like to know contributing factors to trouble understanding formulation. If we remove the hurdle about argumentation vs. not argumentation, doe we then learn about the role of variable names in generalization?
  
  We might pursue a possible difficulty in generalization taking a hint from mathematics education. In mathematics education, single letter variable names are preferred, because the general applicability of the formulation is more obvious. \cite{}
  We might start with an argument whose statements are bound to concrete entities, and shorten the names incrementally, and observe that the argument is retained even as the names are shortened. The small number of observations already made in this approach suggest that the argument might not be seen at all, because it vanishes as soon as the concrete names are altered.
  
  Because generalization and specialization are skills we wish the students to use,
  we might choose to foster these skills explicitly with a course on the development of ontologies.
  This allows us to provide more emphasis on the role of definition. We can note also, in the context, the relative weakness of preconditions associated with the level of a class in a hierarchy. (If we know we are dealing with an Emperor penguin, vs. if we know we are dealing with a bird, vs. an animal, etc.) We can also talk about cases completely covering a space in the same context.
  
  Definitions in terms of more general ones, i.e., add specialization. Proofs about the entities exercises using the definitions when is transformation warranted?
  This course could serve to expedite the introduction of several more advanced courses, such as machine learning, and/or object orientation.
  One important role this course would play is to make students aware of their learning.
  They could view quantitatively the number of properties that are associated with their concepts. 
  They could examine the relationships of which they are aware, from one concept to another, or between a concept and its attributes.
  
  % \paragraph{Explore why they are not convinced}
  % Generalization/abstraction is hard. Literature says occurs with good sleep, which might be rare. Almstrum\cite{almstrum1996investigating} has observed that logic is difficult.
  
  % Why would generalization be hard?
  % Generalization from how many examples?
  % How to distinguish what is a meaningful feature from an insignificant?
  % Supervised/unsupervised learning.
  % In training, explicitly tell what is a meaningful feature. This is definition. Some students don't know they should pay attention.
  % In unsupervised learning, inferences must be drawn from the value of a classification.
  
  % Why is paying attention to definitions hard?
  
  % Scaffold by analogy, or
  % like reading every option and its value set, on UNIX man pages.
  % Variation theory has the purpose of identifying critical aspects / features, by contrasting different variants,
  % red, white and blue potatoes
  % makes clear potatoes have a color attribute,
  % vs. all read potatoes all the time.
  % Allows confusion of red skin with nature of potato.
  
  
  
  %\subsection{Validation at the Level of Phenomenography/Variation Theory}
  
  
  % \subsection{Proofs Using the Pumping Lemma for Regular Languages}
  
  
  \section{Further Enquiries of a Qualitative Nature}
 
 The implications for pedagogy suggest activities that can be tried, and analyzed.
 
 \begin{itemize}
 	\item What internal representations do students use?
 	\item Is there a gamut of internal representations, and does that help with abstraction?
 	\item Concerning mathematization, which is the ability to represent problems in mathematical notation, what do students find is difficult?
 	\item Concerning interiorization, which is the ability to examine and discuss the process of creating proof, what do students find is difficult?
 	\item Concerning comprehension of simple proofs, which is the ability to see that, and why, an argument is convincing, what do students find is difficult?
 	\item Concerning proof analysis, which includes the ability to analyze simple proofs to recognize structure, how involved can a structured composition be, before students begin to have trouble with it?
 	\item Concerning problem recognition, which is the ability to see that a problem is one that matches a known solution technique, how elaborated can a problem statement be, before students cannot recognize it?
 	\item Concerning a transformational approach, which is considering the consequences of varying features of the problem, which step size of transformation is most easily grasped by the students?
 	\item Why is paying attention to definitions hard?
 	\item Concerning the axiomatic approach, which is the exploration of the consequences of definitions, how can we convince students that learning by definition is more efficient than recreating the process of definition building?
 	\item Concerning the construction of valid arguments, which is to synthesize deductions with component parts, including warrants, can we make this more obvious by restricting the set of transformations and warrants that are needed (and telling the students to use only those)?
 	\item Concerning transfer, do students prefer to see the application of proofs in the course in which they are learning proofs, or delay that until the course in which proofs are applied?
 	
 \end{itemize}
 
 \section{Follow-on Enquiries of a Quantitative Nature}
 
 One of the reasons for conducting qualitative studies is though to be development of appropriate questions for quantitative studies.
 Some questions generated by this study that might be suitable to a quantitative study include:
 
 \begin{itemize}
 	\item Are Latino students put at a disadvantage due to culturally insensitive labelling of optional instructional meetings ``Help Sessions''?
 	\item Are different learning approaches such as learn the process steps first and infer the reason afterwards, vs. learn the definitions first, understand the process steps afterwards, rather than memorizing, equally beneficial?
 	\item What percentage of student accept or prefer authoritative sources over use of argumentation?
 	\item What percentage of students can correctly classify a problem as universal vs. existential?
 	\item What percentage of students recognize that working with general, abstract ideas like numbers or graphs has direct implication for specific software development problems?
 	\item Are internalization and interiorization, as described by Harel and Sowder\cite{harel1998students}, less, more or equally distinct in computer science students as in mathematics students?
 	\item Given our concern about generalization, and recent research about the contribution of sleep to generalization\cite{czeisler}, we might wish to compare self-reports about sleep and assessments of ability to notice or create generalization hierarchies.
 	\item Concerning scaffolding and proofs, ask students whether and if so, how, they scaffold their study of proofs with their knowledge of programming.
 	
 	% Draw a distinction between how a program is interpreted or compiled, with
 	%how students decide which step to write next in a program.
 	%That is, we are not using Curry-Howard isomorphism, which is about compilation/interpretation, rather, we are concerned with how students decide what to write when they write code.
 	
 	\item 
 	Anecdotal evidence suggests that pleasantness and fun, which are intrinsic rewards, help students pay attention and remember. Make use of the natural experiment --- some students will have enjoyed the material. Are these the ones who remember better? and does the nature of enjoyment make any difference in understanding productivity aesthetics?
 	\item Variation theory and cognitive science suggest the teacher should make an effort to show positive and negative examples and to point out what causes one to be positive and the other negative to help discern the relevant features. Have you noticed this practice? Did you find it helpful?
 	\item Concerning engagement with the material\\
 	Ask students to rank order the factors that might help them engage with the material\\
 	job related\\
 	prerequisite\\
 	have been curious about\\
 	fun\\
 	competition\\
 	beautiful\\
 	% (Does this happen often)\\
 	% (Does this matter to you?)\\
 	% What, if anything, makes you engage with the material?\\
 	Neurophysiology suggest that animation in overheads makes it easier to be alert to material, that figures draw attention more easily than text.
 	Ask students to comment on what if any things make animation helpful to them, or whether they find some animation helpful.
 	Ask student if they find figures helpful, and if so, to comment on how they help? Do students find it easier to pay attention to figures / animations than to text? Does music help? Is there a kind of music (such as that associated with video games) that helps hold attention?
 \end{itemize}
 

\section{Brochure}\label{brochure}

\subsection{Introduction}

Students need to know that a proof is an argument.\\
Some do, and some do not (list of statements, steps, process)\\

Students need to know that the statement to be proved can have structure, and that
that structure can be profitably be examined to suggest (sometimes quite strongly)
what construction should be followed for the proof.

Students need to know that the proof will be a sequence of warranted transformations
from the premise to the desired consequence, and that some warrants exist because of the definitions of the entities present in the premise and the consequences. (e.g., proofs about trees can involve transformations that are warranted because trees contain no cycles.)

The less-developed end of the range in the students' conceptualizations identifies the starting point of explanatory background material that should be provided.
The needs of the course determine the ending point of the explanatory background 
material.
The major themes in the students' conceptualizations make more evident the 
critical aspects, that distinguish on conceptualization from another, and therefore
suggest the self-assessment questions that should be furnished, to help students know where to begin improving.
An alternative to having analyzed the conceptualizations among the students is to use on a 
student case-by-case basis, a sort of failure modes and effects analysis combined with Bayesian reasoning, whereby the effect of lacking a certain understanding can be predicted to cause a certain pattern of confusion on the part of the
student, and that confusion is used to find the student's zone of proximal development\cite{vygotsky1987zone} and thereby to discover what way is best to help that particular individual.
Different parts of the background material become motivated at different times within the course.
It could help the students to provide a key from possible trouble spots to relevant background material.

\subsection{Brochure Content}
The author believes diagrams aid the abstraction process. The researchers
 tend to believe that students want to learn, and will try to comprehend and to
 become able to apply the material, and that the limitations temporarily present
 in the student can be overcome by explanation and practice.
 
%\subsection{Components of the Learning Objective, in the sense of Marton}

\begin{itemize}
\item Generalization / Specialization: exercise students in the value of generalization, the practice of specialization
\item abstract interpretation
\item use of UML\textsuperscript{\textregistered} class / interface hierarchies
\item multiple representations
\item abstraction is a kind of representation, selecting only certain aspects of interest
\item moving from representation to idea, and 
from idea to different representations
\end{itemize}

\section{Design a Software Engineering Course Featuring Provability as well as Test-Driven Development, Using Conceptualizations}

Awareness of conceptualizations present in the student population can guide us in course preparation.

Suppose we wish to incorporate into our curriculum on software engineering, material on both verification by formal methods, and also code derivation from specifications.
We might wish to have our students able to recognize a specification that can be satisfied
by a transition system, so that they can ascertain that a representation of that transition system that can be converted automatically into code implementation is an available approach.
We would need it to be, that the students were convinced by the mathematical argumentation for the transformations of requirements
to Floyd-Hoare-triples, and to code, could be accomplished.
Knowing the range of the state of preparedness of the incoming students allows us to plan the amount of time to devote to background material,
and which background material should be provided.
Suppose we wished to make use of higher order logic, so that we could employ relations as arguments
to functions.
We might, for example, wish to pass a
graph constraining how a computation should be carried out.
We would like the students to appreciate the mapping between a recursive
implementation and proof by mathematical induction.
We would like the students to discern when a recursion is a tail recursion.
We would like the students to appreciate the mapping between a tail recursion and iteration.
On the one hand we have an idea which mathematical tools we wish to use, and on
the other hand we have an idea 
of the extent of the students' conceptualization.
With these we can begin to design an instructional approach.
\subsection{Recognize a specification that can be satisfied by a transition system}
For this, they should know what a transition system is.
There is a state, so we wish to represent a store, and the states it may take on.
There is a way to change the state, so we wish to represent transitions, and the idea of a path from 
state to state.
They should understand how a transition system can be represented in code, and that this can be carried out automatically.
Path algebra furnishes a rigorous description of these processes.
Elementary path algebra ought to be accessible to the students.
We could introduce (typed) lambda calculus to the students with path algebra as its first use.
Now that we have Java 8 which provides anonymous functions, we can also offer a coded version for
exploration.
Having the use of typed lambda calculus for path algebra, we can then use it to describe the effect of instruction in the context of Floyd-Hoare triples.
Program derivation can be illustrated.
Because we always prefer the students to apply what they comprehend,
it is important to have exercises.
Students should perform derivation, so that they come to appreciate that it can be automated.


\subsection{Composition}
We expect to be able to compose software from components, either in sequence or in parallel, it
is important that the students understand this at a rigorous level.
%To treat functions passed as arguments, procedures to be composed, the need for
%higher order logic is evident. (Check this)
\subsection{Invariants}
The role of invariants in assuring the correctness of composition provides motivation for consideration of invariants.
\subsection{Provability}
With transition systems as a first example of what can be correct by construction,  and invariants
as a tool for provability, students can see that a way to design code with the prospect of fewer bugs is possible, at least in some circumstances.
\subsection{Use of Bridging Material}
The material on mathematical tools we wish to use should be introduced at a level that addresses the 
conceptualizations the students bring to the course.
Because the students bring different levels of preparedness to the class, some
self-assessment might be included, to guide the student to the starting point in the readings corresponding to his or her current ideas.
The self-assessment can make use of the concepts used in the course.
For example, during the course, the idea of invariants is used.
Self-assessment can include questions posed to determine a student's understanding
of the nature and role of an invariant, and direct the student to explanations that may be 
helpful, according to the results of the self-assessment.
From this vantage point, other techniques of proving, including contradiction and contrapositive, are motivated.
%\subsection{Summary}

\subsection{Application of Implications for Pedagogy to a Software Development / Engineering Course}
We use the model of students' conceptualizations shown in  Chapter 4 to provide background material for a course in software engineering organized around the concept of provability-driven development. 
Finding the calculational approach of Gries\cite{gries2012science}, which provides relatively succinct proofs, matching well with the phenomenology of Rota, who found that short proofs were more beautiful and more memorable\cite{rota1997phenomenology}, we prefer this style.
From the range of conceptualizations, we choose to include symbolization, and formation of valid arguments stressing that rules of inference satisfy guards upon the transformations we can make as we transition from one statement to another.

Material addressed to a student reader uses the second person pronoun, ``you''.

Some multiple choice questions follow.
\fbox{\begin{minipage}{15em}
Please note that the questions have been designed to help you notice the content being explored. If you find that the phrasing of the questions is helping you arrive at the correct answer, you should choose to study the material. Variables, which can be individual letters, or names, either in computer programs or mathematical statements, are used to represent ideas.


Which of the following describes a while loop executing?\\
boolean done = false;\\
while(!done)\{\\
statements which eventually change done to true\}

\begin{itemize}
\item ($\neg$ done)(statements)(done)
\item ($\neg d$)(statements)(d)
\item($\neg$p)(statements)(p)
\item(p)(statements)($\neg$p)
\item all of the above
\item none of the above
\end{itemize}

Which of the following describes two statements executing in sequence (where, for any $i$, $s_i$ denotes a state of the variables being used by the program)? Please note that reading the value of variable does not change the state.

\begin{itemize}
\item (in state $s_0$)(print ``Hello, world'')(print x) (in state $s_0$)
\item (in state $s_0$)(x=x+1)(print x) (in state $s_0$)
\item (in state $s_0$)(x=x+1)(print x) (in state $s_1$)
\item 1 and 3 but not 2
\end{itemize}
\end{minipage}}

 In programs, meaningful
variable names have been shown to increase the speed and correctness of comprehension \cite{gellenbeck1991investigation}. In mathematical statements, single letter variable names have been shown to improve the skill of abstraction.
Thus we choose to employ meaningful variable names for now, but will tend to replace them with single letters later.
You have probably seen variables in high school algebra, for example in the equation for a line, typically written as $y=mx+b$.
Here, $y$, the vertical position on a graph, is calculated from $m$, the slope of the line, and $b$, the vertical offset when $x=0$. A family of parallel lines can be generated by keeping one value for $m$, and setting different values for $b$.
Thus we see that a variable can refer to a single value, and a variable can also refer to different single values at a time.
For any one point along a line, when the value of $x$ refers to a single value, the single values of $x,m$ and $b$ can be used to calculate a single value for $y$. 
It is, however, also possible to think of the values of horizontal axis all together, and refer to that idea by a single variable $x$.
If you are familiar with a programming language, such as MATLAB\textsuperscript{\textregistered}, that supports vector variables, you will have seen single variable that can refer to many individual values at once.
Likewise, you may have worked with arrays of one ore more dimensions; reflecting on this, the array name (without specified indices) can be though of as referring to the entire array.
Keeping that idea in mind, we can contemplate the mathematical expression $0 \leq x \leq 1$.
When $x$ is an integer, we have that the integers 0 and 1 satisfy this description.
Depending upon context, $x$ may represent the range including these.
changing the universe of discourse from integers to reals, the expression $x<3$ represents, depending upon context, not necessarily only a single, yet-to-be-determined real number that also has the property of being less than 3, but also it can be that $x$ represents all real numbers less than 3.


\subsection{Logical Operators}
We wish students to understand strengthening and weakening of conditions.
We wish student to understand the idea of a precondition as a disclaimer, and also as a guard.
We wish students to be able to negate statements with multiple quantifiers.
We have seen from investigating the conceptualizations that students can have trouble even negating statements with single quantifiers.
\subsection{Relations}
We want students to understand relations, because we want them to see the pairing of an input state and an output state, as a result of a transformation by a computation, as a relation.
\subsection{Rules of Inference}
Calculational proofs\cite{dijkstra2012predicate} seem to suggest strongly the way to proceed.
Stepping through examples of these might help students comprehend.
\subsection{Internalization and Interiorization}
Recall that internalization has been achieved when a student can perform a process correctly, not necessarily recognizing the  circumstances in which that process is appropriate.
What distinguishes interiorization from internalization is that the student can examine and discuss the process, beyond being able to  carry it out.


We might imagine that students of computer science would be familiar with thinking about processes, and so would become able to discuss processes quickly moving from internalization to interiorization but the data disagree.
Students readily acquire the internalization conceptualization, but linger there.
(One notes in passing that full marks can be achieved
by following the procedure even if it is not understood.)
Understanding that argumentation is occurring that the validity of the argument depends upon logic, in the case of proof by mathematic induction, the connection between the base case and inductive step. Almstrum\cite{almstrum1996investigating} has shown that students of computer science find logic relatively difficult.

It is important for the software engineering course that students can examine and discuss the process of program derivation from requirements.
Recognition of the  circumstances in which automatic program derivation can be performed is an important part of understanding requirements.
We combine internalization and interiorization because our interviews have not addressed topics that the participants cannot discuss.
We have however found student testimony that process that can be carried out confidently are nevertheless not used due to lack of a means to determine whether the process is appropriate to circumstances.

\fbox{\begin{minipage}{15em}
Which, if any, of the requirements described below can be satisfied by a finite state machine?

\begin{itemize}
\item Recognize whether or not a string could have been generated by a regular expression
\item Recognize whether or not a string could have been generated by at least one of a set of regular expressions
\item Recognize whether or not a string could have been generated by juxtaposition of strings, each of which could have been generated by at least one of a set of regular expressions
\item all of the above
\item none of the above
\end{itemize}
Is this a mapping from a recursive algorithm to a proof by mathematical induction?
The base case or cases of the recursive definition map to the base case or cases of the proof, and the recursive call or calls are always invoking with a problem of a smaller size, and the inductive step is always working with a premise that is assumed to be true.
In both recursive algorithms and inductive steps, the next problem is solved making use of a previous solution.
Is this a mapping from a concrete example of a proof to a proof in a more abstract circumstance?\\
Concrete\\
There is a commercially available car, a deLorean.\\
There is an  unreachable goal, time-travel.\\
Spielberg has shown us that if only we had a ``flux-capacitor'' to attach to the deLorean, we could have time-travel.\\
Therefore we conclude that the flux-capacitor must also be unreachable, by the following logic:\\
If we had the flux-capacitor and the deLorean, we would get time travel.\\
We cannot get time-travel.\\
So, we cannot have the flux-capacitor and the ddLorean.\\
We can get the deLorean.\\
So, it must be that we cannot get the flux-capacitor.\\
Relatively Abstract\\
There is a simple algorithm, $M$, by which we can determine whether two finite sets have any elements in common.\\
There is an unreachable goal, $A_{TM}$.\\
Sipser has shown us that, if only we had $E_TM$ and $M$, we could have $A_{TM}$.\\
We cannot get $A_{TM}$.\\
So, we cannot have $E_{TM}$ together with $M$.\\
We can have $M$.\\
So, it must be that we cannot get $E_{TM}$.\\
(I'm thinking pictures would help.)
In symbols:\\
$\neg A_{TM}$\\
$M \land E_{TM} \rightarrow A_{TM} $\\
$\neg A_{TM} \rightarrow \neg(M \land E_{TM})$\\
$\neg(M \land E_{TM})$\\
$\neg M \lor \neg E_{TM}$\\
$M$\\
$\neg E_{TM}$
\end{minipage}}

%\subsection{Perceptual}
%\subsection{Transformational}
%\subsection{Axiomatic}
%To detect
\subsection{What Do You Say After You Say HelloWorld?}
This is a software engineering course, organized around the idea of provability driven development.
We want to impart the desire to approach software engineering problems with methods of formalizing calculation checking.
Mathematics provides what is necessary for proofs, by means that include precise definitions.
We would write definitions of program function in a style admitting proof.
We will use finite automata.
So, a section on proof, followed by a section on finite automata, formal definitions of things we use,
clients, servers, files, streams, What sort of things are we aiming to prove?
liveness, safety, accuracy, i/o relations for component based systems resource utilization including time utility functions.
The construction technique needs to be proven.
Several techniques for this are under development and/or in use:
BL, statecharts, Wise computing. These permit composition of systems.

%Unlink (in a book on formal methods) Wing, we do not pick one, rather, we relate (multiple possibilities to one another?) them, like ISO standard communication stack and those defined things live in the space of abstractions, i.e., many different operational sequences covered by one invariant.
%What impact does provability have on these?
%structure in types data structures meets provability (recursive data structure, proof by induction)
%can we represent data structures as finite automata?
%Is there a reason why not to do this? e.g., would it not be sufficiently general?
%representing datatypes with algebras Hoare 1985 Milner 1980 models, \cite{milner1978theory} with math, might have more properties that we want to use, vs.
%theories, with which we create only our desired properties.
%Z, VDM, emphasize models over theories,
%Z VDM Larch algebraic specification language would we want to use Tempo instead of OBJ?
A formal method has an assertion language, for example, first order predicate logic.
A formal method has a specification language, which in turn has a syntax and a semantics.
The syntax contains rules for formulating syntactically correct (legal) terms.

Mitchell \cite[p. 35]{mitchell1996foundations}, in Foundation of Programming Languages, says Hilbert-style proofs system consists of axioms and proof rules.
Axioms are provable by definition.
A proof is a structured object built from formulae, according to constraints established by a set of axioms and rules of inference.

Arcavi et al.\cite[p. 56]{arcavi1998teaching}'s work in cognitive science\cite{mcleod1992research} has shown that students' beliefs about the nature of a subject may have profound effects on their learning of it. % (McLeod 1992) Research of affect in mathmatics education: A reconceptualization In Doublas A. Grouws (Ed.) Handbook of research on mathematics teaching and learning [pp. 575-596 NY Macmillan]

One approach to teaching students to generalize is used by Schoenfeld\cite{schoenfeld1993learning,schoenfeld1994we,schoenfeld1998reflections} (page 60 and earlier), who teaches his students heuristics, including one from Polya\cite{polya1954mathematics}, about problems with fewer requirements. 

Researchers including Cipra\cite{cipra1995bumpy} and Culotta\cite{culotta1992calculus} have noticed that students, having learned procedures, have not necessarily learned to apply them. 
%Cipra 1995 UME Trends The bumpy road to reform 
%Culotta 1992 The calculus of education reform science 255



% \subsection{Domain, Range, Mapping, Relation, Function, Equivalence in Proofs}
% This part of the study contributes to recognition and comprehension.
 
% For the study about domain, range, mapping, relation, function and equivalence in proofs, students
% taking, or having taken, discrete systems, especially students who
% had sought help while taking introductory object oriented programming volunteered
% to be interviewed.
%  \subsubsection{Expanded semi-structured interview protocol for domain, range, language, equivalence class in Proofs}
%  \subsubsection{Expanded semi-structured interview protocol for definitions, language, reasoning in Proofs}